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

Definition df-hba 26457
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 26487). 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 26655. (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 26407 . 2  class  ~H
2 cva 26408 . . . . 5  class  +h
3 csm 26409 . . . . 5  class  .h
42, 3cop 4008 . . . 4  class  <.  +h  ,  .h  >.
5 cno 26411 . . . 4  class  normh
64, 5cop 4008 . . 3  class  <. <.  +h  ,  .h  >. ,  normh >.
7 cba 26050 . . 3  class  BaseSet
86, 7cfv 5601 . 2  class  ( BaseSet `  <. <.  +h  ,  .h  >. ,  normh >. )
91, 8wceq 1437 1  wff  ~H  =  ( BaseSet `  <. <.  +h  ,  .h  >. ,  normh >. )
Colors of variables: wff setvar class
This definition is referenced by:  axhilex-zf  26469  axhfvadd-zf  26470  axhvcom-zf  26471  axhvass-zf  26472  axhv0cl-zf  26473  axhvaddid-zf  26474  axhfvmul-zf  26475  axhvmulid-zf  26476  axhvmulass-zf  26477  axhvdistr1-zf  26478  axhvdistr2-zf  26479  axhvmul0-zf  26480  axhfi-zf  26481  axhis1-zf  26482  axhis2-zf  26483  axhis3-zf  26484  axhis4-zf  26485  axhcompl-zf  26486  bcsiHIL  26668  hlimadd  26681  hhssabloi  26748  pjhthlem2  26880  nmopsetretHIL  27352  nmopub2tHIL  27398  hmopbdoptHIL  27476
  Copyright terms: Public domain W3C validator