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

Definition df-hba 28741
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 28771). Note that 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 28939. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)
Assertion
Ref Expression
df-hba ℋ = (BaseSet‘⟨⟨ + , · ⟩, norm⟩)

Detailed syntax breakdown of Definition df-hba
StepHypRef Expression
1 chba 28691 . 2 class
2 cva 28692 . . . . 5 class +
3 csm 28693 . . . . 5 class ·
42, 3cop 4554 . . . 4 class ⟨ + , ·
5 cno 28695 . . . 4 class norm
64, 5cop 4554 . . 3 class ⟨⟨ + , · ⟩, norm
7 cba 28358 . . 3 class BaseSet
86, 7cfv 6336 . 2 class (BaseSet‘⟨⟨ + , · ⟩, norm⟩)
91, 8wceq 1538 1 wff ℋ = (BaseSet‘⟨⟨ + , · ⟩, norm⟩)
Colors of variables: wff setvar class
This definition is referenced by:  axhilex-zf  28753  axhfvadd-zf  28754  axhvcom-zf  28755  axhvass-zf  28756  axhv0cl-zf  28757  axhvaddid-zf  28758  axhfvmul-zf  28759  axhvmulid-zf  28760  axhvmulass-zf  28761  axhvdistr1-zf  28762  axhvdistr2-zf  28763  axhvmul0-zf  28764  axhfi-zf  28765  axhis1-zf  28766  axhis2-zf  28767  axhis3-zf  28768  axhis4-zf  28769  axhcompl-zf  28770  bcsiHIL  28952  hlimadd  28965  hhssabloilem  29033  pjhthlem2  29164  nmopsetretHIL  29636  nmopub2tHIL  29682  hmopbdoptHIL  29760
  Copyright terms: Public domain W3C validator