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

Definition df-hba 25751
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 25781). 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 25949. (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 25701 . 2  class  ~H
2 cva 25702 . . . . 5  class  +h
3 csm 25703 . . . . 5  class  .h
42, 3cop 4016 . . . 4  class  <.  +h  ,  .h  >.
5 cno 25705 . . . 4  class  normh
64, 5cop 4016 . . 3  class  <. <.  +h  ,  .h  >. ,  normh >.
7 cba 25344 . . 3  class  BaseSet
86, 7cfv 5574 . 2  class  ( BaseSet `  <. <.  +h  ,  .h  >. ,  normh >. )
91, 8wceq 1381 1  wff  ~H  =  ( BaseSet `  <. <.  +h  ,  .h  >. ,  normh >. )
Colors of variables: wff setvar class
This definition is referenced by:  axhilex-zf  25763  axhfvadd-zf  25764  axhvcom-zf  25765  axhvass-zf  25766  axhv0cl-zf  25767  axhvaddid-zf  25768  axhfvmul-zf  25769  axhvmulid-zf  25770  axhvmulass-zf  25771  axhvdistr1-zf  25772  axhvdistr2-zf  25773  axhvmul0-zf  25774  axhfi-zf  25775  axhis1-zf  25776  axhis2-zf  25777  axhis3-zf  25778  axhis4-zf  25779  axhcompl-zf  25780  bcsiHIL  25962  hlimadd  25975  hhssabloi  26043  pjhthlem2  26175  nmopsetretHIL  26648  nmopub2tHIL  26694  hmopbdoptHIL  26772
  Copyright terms: Public domain W3C validator