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

Definition df-hba 25562
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 25592). 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 25760. (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 25512 . 2  class  ~H
2 cva 25513 . . . . 5  class  +h
3 csm 25514 . . . . 5  class  .h
42, 3cop 4033 . . . 4  class  <.  +h  ,  .h  >.
5 cno 25516 . . . 4  class  normh
64, 5cop 4033 . . 3  class  <. <.  +h  ,  .h  >. ,  normh >.
7 cba 25155 . . 3  class  BaseSet
86, 7cfv 5586 . 2  class  ( BaseSet `  <. <.  +h  ,  .h  >. ,  normh >. )
91, 8wceq 1379 1  wff  ~H  =  ( BaseSet `  <. <.  +h  ,  .h  >. ,  normh >. )
Colors of variables: wff setvar class
This definition is referenced by:  axhilex-zf  25574  axhfvadd-zf  25575  axhvcom-zf  25576  axhvass-zf  25577  axhv0cl-zf  25578  axhvaddid-zf  25579  axhfvmul-zf  25580  axhvmulid-zf  25581  axhvmulass-zf  25582  axhvdistr1-zf  25583  axhvdistr2-zf  25584  axhvmul0-zf  25585  axhfi-zf  25586  axhis1-zf  25587  axhis2-zf  25588  axhis3-zf  25589  axhis4-zf  25590  axhcompl-zf  25591  bcsiHIL  25773  hlimadd  25786  hhssabloi  25854  pjhthlem2  25986  nmopsetretHIL  26459  nmopub2tHIL  26505  hmopbdoptHIL  26583
  Copyright terms: Public domain W3C validator