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

Definition df-hba 21549
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 21579). 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 as theorem hhba 21746. (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 21499 . 2  class  ~H
2 cva 21500 . . . . 5  class  +h
3 csm 21501 . . . . 5  class  .h
42, 3cop 3643 . . . 4  class  <.  +h  ,  .h  >.
5 cno 21503 . . . 4  class  normh
64, 5cop 3643 . . 3  class  <. <.  +h  ,  .h  >. ,  normh >.
7 cba 21142 . . 3  class  BaseSet
86, 7cfv 5255 . 2  class  ( BaseSet `  <. <.  +h  ,  .h  >. ,  normh >. )
91, 8wceq 1623 1  wff  ~H  =  ( BaseSet `  <. <.  +h  ,  .h  >. ,  normh >. )
Colors of variables: wff set class
This definition is referenced by:  axhilex-zf  21561  axhfvadd-zf  21562  axhvcom-zf  21563  axhvass-zf  21564  axhv0cl-zf  21565  axhvaddid-zf  21566  axhfvmul-zf  21567  axhvmulid-zf  21568  axhvmulass-zf  21569  axhvdistr1-zf  21570  axhvdistr2-zf  21571  axhvmul0-zf  21572  axhfi-zf  21573  axhis1-zf  21574  axhis2-zf  21575  axhis3-zf  21576  axhis4-zf  21577  axhcompl-zf  21578  bcsiHIL  21759  hlimadd  21772  hhssabloi  21839  pjhthlem2  21971  nmopsetretHIL  22444  nmopub2tHIL  22490  hmopbdoptHIL  22568
  Copyright terms: Public domain W3C validator