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

Definition df-hba 24194
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 24224). 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 24392. (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 24144 . 2  class  ~H
2 cva 24145 . . . . 5  class  +h
3 csm 24146 . . . . 5  class  .h
42, 3cop 3871 . . . 4  class  <.  +h  ,  .h  >.
5 cno 24148 . . . 4  class  normh
64, 5cop 3871 . . 3  class  <. <.  +h  ,  .h  >. ,  normh >.
7 cba 23787 . . 3  class  BaseSet
86, 7cfv 5406 . 2  class  ( BaseSet `  <. <.  +h  ,  .h  >. ,  normh >. )
91, 8wceq 1362 1  wff  ~H  =  ( BaseSet `  <. <.  +h  ,  .h  >. ,  normh >. )
Colors of variables: wff setvar class
This definition is referenced by:  axhilex-zf  24206  axhfvadd-zf  24207  axhvcom-zf  24208  axhvass-zf  24209  axhv0cl-zf  24210  axhvaddid-zf  24211  axhfvmul-zf  24212  axhvmulid-zf  24213  axhvmulass-zf  24214  axhvdistr1-zf  24215  axhvdistr2-zf  24216  axhvmul0-zf  24217  axhfi-zf  24218  axhis1-zf  24219  axhis2-zf  24220  axhis3-zf  24221  axhis4-zf  24222  axhcompl-zf  24223  bcsiHIL  24405  hlimadd  24418  hhssabloi  24486  pjhthlem2  24618  nmopsetretHIL  25091  nmopub2tHIL  25137  hmopbdoptHIL  25215
  Copyright terms: Public domain W3C validator