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

Definition df-hba 21545
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 21575). 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 21742. (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 21495 . 2  class  ~H
2 cva 21496 . . . . 5  class  +h
3 csm 21497 . . . . 5  class  .h
42, 3cop 3644 . . . 4  class  <.  +h  ,  .h  >.
5 cno 21499 . . . 4  class  normh
64, 5cop 3644 . . 3  class  <. <.  +h  ,  .h  >. ,  normh >.
7 cba 21136 . . 3  class  BaseSet
86, 7cfv 5221 . 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  21557  axhfvadd-zf  21558  axhvcom-zf  21559  axhvass-zf  21560  axhv0cl-zf  21561  axhvaddid-zf  21562  axhfvmul-zf  21563  axhvmulid-zf  21564  axhvmulass-zf  21565  axhvdistr1-zf  21566  axhvdistr2-zf  21567  axhvmul0-zf  21568  axhfi-zf  21569  axhis1-zf  21570  axhis2-zf  21571  axhis3-zf  21572  axhis4-zf  21573  axhcompl-zf  21574  bcsiHIL  21755  hlimadd  21768  hhssabloi  21835  pjhthlem2  21967  nmopsetretHIL  22440  nmopub2tHIL  22486  hmopbdoptHIL  22564
  Copyright terms: Public domain W3C validator