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

Definition df-hba 26671
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 26701). 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 26869. (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 26621 . 2  class  ~H
2 cva 26622 . . . . 5  class  +h
3 csm 26623 . . . . 5  class  .h
42, 3cop 3986 . . . 4  class  <.  +h  ,  .h  >.
5 cno 26625 . . . 4  class  normh
64, 5cop 3986 . . 3  class  <. <.  +h  ,  .h  >. ,  normh >.
7 cba 26254 . . 3  class  BaseSet
86, 7cfv 5601 . 2  class  ( BaseSet `  <. <.  +h  ,  .h  >. ,  normh >. )
91, 8wceq 1455 1  wff  ~H  =  ( BaseSet `  <. <.  +h  ,  .h  >. ,  normh >. )
Colors of variables: wff setvar class
This definition is referenced by:  axhilex-zf  26683  axhfvadd-zf  26684  axhvcom-zf  26685  axhvass-zf  26686  axhv0cl-zf  26687  axhvaddid-zf  26688  axhfvmul-zf  26689  axhvmulid-zf  26690  axhvmulass-zf  26691  axhvdistr1-zf  26692  axhvdistr2-zf  26693  axhvmul0-zf  26694  axhfi-zf  26695  axhis1-zf  26696  axhis2-zf  26697  axhis3-zf  26698  axhis4-zf  26699  axhcompl-zf  26700  bcsiHIL  26882  hlimadd  26895  hhssabloi  26962  pjhthlem2  27094  nmopsetretHIL  27566  nmopub2tHIL  27612  hmopbdoptHIL  27690
  Copyright terms: Public domain W3C validator