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

Definition df-hba 21565
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 21595). 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 21762. (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 21515 . 2  class  ~H
2 cva 21516 . . . . 5  class  +h
3 csm 21517 . . . . 5  class  .h
42, 3cop 3656 . . . 4  class  <.  +h  ,  .h  >.
5 cno 21519 . . . 4  class  normh
64, 5cop 3656 . . 3  class  <. <.  +h  ,  .h  >. ,  normh >.
7 cba 21158 . . 3  class  BaseSet
86, 7cfv 5271 . 2  class  ( BaseSet `  <. <.  +h  ,  .h  >. ,  normh >. )
91, 8wceq 1632 1  wff  ~H  =  ( BaseSet `  <. <.  +h  ,  .h  >. ,  normh >. )
Colors of variables: wff set class
This definition is referenced by:  axhilex-zf  21577  axhfvadd-zf  21578  axhvcom-zf  21579  axhvass-zf  21580  axhv0cl-zf  21581  axhvaddid-zf  21582  axhfvmul-zf  21583  axhvmulid-zf  21584  axhvmulass-zf  21585  axhvdistr1-zf  21586  axhvdistr2-zf  21587  axhvmul0-zf  21588  axhfi-zf  21589  axhis1-zf  21590  axhis2-zf  21591  axhis3-zf  21592  axhis4-zf  21593  axhcompl-zf  21594  bcsiHIL  21775  hlimadd  21788  hhssabloi  21855  pjhthlem2  21987  nmopsetretHIL  22460  nmopub2tHIL  22506  hmopbdoptHIL  22584
  Copyright terms: Public domain W3C validator