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

Definition df-hba 22321
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 22351). 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 22518. (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 22271 . 2  class  ~H
2 cva 22272 . . . . 5  class  +h
3 csm 22273 . . . . 5  class  .h
42, 3cop 3761 . . . 4  class  <.  +h  ,  .h  >.
5 cno 22275 . . . 4  class  normh
64, 5cop 3761 . . 3  class  <. <.  +h  ,  .h  >. ,  normh >.
7 cba 21914 . . 3  class  BaseSet
86, 7cfv 5395 . 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  22333  axhfvadd-zf  22334  axhvcom-zf  22335  axhvass-zf  22336  axhv0cl-zf  22337  axhvaddid-zf  22338  axhfvmul-zf  22339  axhvmulid-zf  22340  axhvmulass-zf  22341  axhvdistr1-zf  22342  axhvdistr2-zf  22343  axhvmul0-zf  22344  axhfi-zf  22345  axhis1-zf  22346  axhis2-zf  22347  axhis3-zf  22348  axhis4-zf  22349  axhcompl-zf  22350  bcsiHIL  22531  hlimadd  22544  hhssabloi  22611  pjhthlem2  22743  nmopsetretHIL  23216  nmopub2tHIL  23262  hmopbdoptHIL  23340
  Copyright terms: Public domain W3C validator