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

Definition df-hba 21551
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 21581). 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 21748. (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 21501 . 2  class  ~H
2 cva 21502 . . . . 5  class  +h
3 csm 21503 . . . . 5  class  .h
42, 3cop 3645 . . . 4  class  <.  +h  ,  .h  >.
5 cno 21505 . . . 4  class  normh
64, 5cop 3645 . . 3  class  <. <.  +h  ,  .h  >. ,  normh >.
7 cba 21144 . . 3  class  BaseSet
86, 7cfv 5257 . 2  class  ( BaseSet `  <. <.  +h  ,  .h  >. ,  normh >. )
91, 8wceq 1625 1  wff  ~H  =  ( BaseSet `  <. <.  +h  ,  .h  >. ,  normh >. )
Colors of variables: wff set class
This definition is referenced by:  axhilex-zf  21563  axhfvadd-zf  21564  axhvcom-zf  21565  axhvass-zf  21566  axhv0cl-zf  21567  axhvaddid-zf  21568  axhfvmul-zf  21569  axhvmulid-zf  21570  axhvmulass-zf  21571  axhvdistr1-zf  21572  axhvdistr2-zf  21573  axhvmul0-zf  21574  axhfi-zf  21575  axhis1-zf  21576  axhis2-zf  21577  axhis3-zf  21578  axhis4-zf  21579  axhcompl-zf  21580  bcsiHIL  21761  hlimadd  21774  hhssabloi  21841  pjhthlem2  21973  nmopsetretHIL  22446  nmopub2tHIL  22492  hmopbdoptHIL  22570
  Copyright terms: Public domain W3C validator