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

Definition df-hba 26087
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 26117). 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 26285. (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 26037 . 2  class  ~H
2 cva 26038 . . . . 5  class  +h
3 csm 26039 . . . . 5  class  .h
42, 3cop 4022 . . . 4  class  <.  +h  ,  .h  >.
5 cno 26041 . . . 4  class  normh
64, 5cop 4022 . . 3  class  <. <.  +h  ,  .h  >. ,  normh >.
7 cba 25680 . . 3  class  BaseSet
86, 7cfv 5570 . 2  class  ( BaseSet `  <. <.  +h  ,  .h  >. ,  normh >. )
91, 8wceq 1398 1  wff  ~H  =  ( BaseSet `  <. <.  +h  ,  .h  >. ,  normh >. )
Colors of variables: wff setvar class
This definition is referenced by:  axhilex-zf  26099  axhfvadd-zf  26100  axhvcom-zf  26101  axhvass-zf  26102  axhv0cl-zf  26103  axhvaddid-zf  26104  axhfvmul-zf  26105  axhvmulid-zf  26106  axhvmulass-zf  26107  axhvdistr1-zf  26108  axhvdistr2-zf  26109  axhvmul0-zf  26110  axhfi-zf  26111  axhis1-zf  26112  axhis2-zf  26113  axhis3-zf  26114  axhis4-zf  26115  axhcompl-zf  26116  bcsiHIL  26298  hlimadd  26311  hhssabloi  26379  pjhthlem2  26511  nmopsetretHIL  26984  nmopub2tHIL  27030  hmopbdoptHIL  27108
  Copyright terms: Public domain W3C validator