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

Definition df-hba 24524
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 24554). 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 24722. (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 24474 . 2  class  ~H
2 cva 24475 . . . . 5  class  +h
3 csm 24476 . . . . 5  class  .h
42, 3cop 3992 . . . 4  class  <.  +h  ,  .h  >.
5 cno 24478 . . . 4  class  normh
64, 5cop 3992 . . 3  class  <. <.  +h  ,  .h  >. ,  normh >.
7 cba 24117 . . 3  class  BaseSet
86, 7cfv 5527 . 2  class  ( BaseSet `  <. <.  +h  ,  .h  >. ,  normh >. )
91, 8wceq 1370 1  wff  ~H  =  ( BaseSet `  <. <.  +h  ,  .h  >. ,  normh >. )
Colors of variables: wff setvar class
This definition is referenced by:  axhilex-zf  24536  axhfvadd-zf  24537  axhvcom-zf  24538  axhvass-zf  24539  axhv0cl-zf  24540  axhvaddid-zf  24541  axhfvmul-zf  24542  axhvmulid-zf  24543  axhvmulass-zf  24544  axhvdistr1-zf  24545  axhvdistr2-zf  24546  axhvmul0-zf  24547  axhfi-zf  24548  axhis1-zf  24549  axhis2-zf  24550  axhis3-zf  24551  axhis4-zf  24552  axhcompl-zf  24553  bcsiHIL  24735  hlimadd  24748  hhssabloi  24816  pjhthlem2  24948  nmopsetretHIL  25421  nmopub2tHIL  25467  hmopbdoptHIL  25545
  Copyright terms: Public domain W3C validator