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

Definition df-hba 21862
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 21892). 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 22059. (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 21812 . 2  class  ~H
2 cva 21813 . . . . 5  class  +h
3 csm 21814 . . . . 5  class  .h
42, 3cop 3732 . . . 4  class  <.  +h  ,  .h  >.
5 cno 21816 . . . 4  class  normh
64, 5cop 3732 . . 3  class  <. <.  +h  ,  .h  >. ,  normh >.
7 cba 21455 . . 3  class  BaseSet
86, 7cfv 5358 . 2  class  ( BaseSet `  <. <.  +h  ,  .h  >. ,  normh >. )
91, 8wceq 1647 1  wff  ~H  =  ( BaseSet `  <. <.  +h  ,  .h  >. ,  normh >. )
Colors of variables: wff set class
This definition is referenced by:  axhilex-zf  21874  axhfvadd-zf  21875  axhvcom-zf  21876  axhvass-zf  21877  axhv0cl-zf  21878  axhvaddid-zf  21879  axhfvmul-zf  21880  axhvmulid-zf  21881  axhvmulass-zf  21882  axhvdistr1-zf  21883  axhvdistr2-zf  21884  axhvmul0-zf  21885  axhfi-zf  21886  axhis1-zf  21887  axhis2-zf  21888  axhis3-zf  21889  axhis4-zf  21890  axhcompl-zf  21891  bcsiHIL  22072  hlimadd  22085  hhssabloi  22152  pjhthlem2  22284  nmopsetretHIL  22757  nmopub2tHIL  22803  hmopbdoptHIL  22881
  Copyright terms: Public domain W3C validator