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

Definition df-hba 22474
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 22504). 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 22671. (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 22424 . 2  class  ~H
2 cva 22425 . . . . 5  class  +h
3 csm 22426 . . . . 5  class  .h
42, 3cop 3819 . . . 4  class  <.  +h  ,  .h  >.
5 cno 22428 . . . 4  class  normh
64, 5cop 3819 . . 3  class  <. <.  +h  ,  .h  >. ,  normh >.
7 cba 22067 . . 3  class  BaseSet
86, 7cfv 5456 . 2  class  ( BaseSet `  <. <.  +h  ,  .h  >. ,  normh >. )
91, 8wceq 1653 1  wff  ~H  =  ( BaseSet `  <. <.  +h  ,  .h  >. ,  normh >. )
Colors of variables: wff set class
This definition is referenced by:  axhilex-zf  22486  axhfvadd-zf  22487  axhvcom-zf  22488  axhvass-zf  22489  axhv0cl-zf  22490  axhvaddid-zf  22491  axhfvmul-zf  22492  axhvmulid-zf  22493  axhvmulass-zf  22494  axhvdistr1-zf  22495  axhvdistr2-zf  22496  axhvmul0-zf  22497  axhfi-zf  22498  axhis1-zf  22499  axhis2-zf  22500  axhis3-zf  22501  axhis4-zf  22502  axhcompl-zf  22503  bcsiHIL  22684  hlimadd  22697  hhssabloi  22764  pjhthlem2  22896  nmopsetretHIL  23369  nmopub2tHIL  23415  hmopbdoptHIL  23493
  Copyright terms: Public domain W3C validator