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

Definition df-hba 22425
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 22455). 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 22622. (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 22375 . 2  class  ~H
2 cva 22376 . . . . 5  class  +h
3 csm 22377 . . . . 5  class  .h
42, 3cop 3777 . . . 4  class  <.  +h  ,  .h  >.
5 cno 22379 . . . 4  class  normh
64, 5cop 3777 . . 3  class  <. <.  +h  ,  .h  >. ,  normh >.
7 cba 22018 . . 3  class  BaseSet
86, 7cfv 5413 . 2  class  ( BaseSet `  <. <.  +h  ,  .h  >. ,  normh >. )
91, 8wceq 1649 1  wff  ~H  =  ( BaseSet `  <. <.  +h  ,  .h  >. ,  normh >. )
Colors of variables: wff set class
This definition is referenced by:  axhilex-zf  22437  axhfvadd-zf  22438  axhvcom-zf  22439  axhvass-zf  22440  axhv0cl-zf  22441  axhvaddid-zf  22442  axhfvmul-zf  22443  axhvmulid-zf  22444  axhvmulass-zf  22445  axhvdistr1-zf  22446  axhvdistr2-zf  22447  axhvmul0-zf  22448  axhfi-zf  22449  axhis1-zf  22450  axhis2-zf  22451  axhis3-zf  22452  axhis4-zf  22453  axhcompl-zf  22454  bcsiHIL  22635  hlimadd  22648  hhssabloi  22715  pjhthlem2  22847  nmopsetretHIL  23320  nmopub2tHIL  23366  hmopbdoptHIL  23444
  Copyright terms: Public domain W3C validator