HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  df-hba Structured version   Unicode version

Definition df-hba 24322
Description: Define base set of Hilbert space, for use if we want to develop Hilbert space independently from the axioms (see comments in ax-hilex 24352). Note that  ~H is considered a primitive in the Hilbert space axioms below, and we don't use this definition outside of this section. This definition can be proved independently from those axioms as theorem hhba 24520. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
Assertion
Ref Expression
df-hba  |-  ~H  =  ( BaseSet `  <. <.  +h  ,  .h  >. ,  normh >. )

Detailed syntax breakdown of Definition df-hba
StepHypRef Expression
1 chil 24272 . 2  class  ~H
2 cva 24273 . . . . 5  class  +h
3 csm 24274 . . . . 5  class  .h
42, 3cop 3878 . . . 4  class  <.  +h  ,  .h  >.
5 cno 24276 . . . 4  class  normh
64, 5cop 3878 . . 3  class  <. <.  +h  ,  .h  >. ,  normh >.
7 cba 23915 . . 3  class  BaseSet
86, 7cfv 5413 . 2  class  ( BaseSet `  <. <.  +h  ,  .h  >. ,  normh >. )
91, 8wceq 1369 1  wff  ~H  =  ( BaseSet `  <. <.  +h  ,  .h  >. ,  normh >. )
Colors of variables: wff setvar class
This definition is referenced by:  axhilex-zf  24334  axhfvadd-zf  24335  axhvcom-zf  24336  axhvass-zf  24337  axhv0cl-zf  24338  axhvaddid-zf  24339  axhfvmul-zf  24340  axhvmulid-zf  24341  axhvmulass-zf  24342  axhvdistr1-zf  24343  axhvdistr2-zf  24344  axhvmul0-zf  24345  axhfi-zf  24346  axhis1-zf  24347  axhis2-zf  24348  axhis3-zf  24349  axhis4-zf  24350  axhcompl-zf  24351  bcsiHIL  24533  hlimadd  24546  hhssabloi  24614  pjhthlem2  24746  nmopsetretHIL  25219  nmopub2tHIL  25265  hmopbdoptHIL  25343
  Copyright terms: Public domain W3C validator