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 28176
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 28206). 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 28374. (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 chil 28126 . 2 class
2 cva 28127 . . . . 5 class +
3 csm 28128 . . . . 5 class ·
42, 3cop 4387 . . . 4 class ⟨ + , ·
5 cno 28130 . . . 4 class norm
64, 5cop 4387 . . 3 class ⟨⟨ + , · ⟩, norm
7 cba 27791 . . 3 class BaseSet
86, 7cfv 6110 . 2 class (BaseSet‘⟨⟨ + , · ⟩, norm⟩)
91, 8wceq 1637 1 wff ℋ = (BaseSet‘⟨⟨ + , · ⟩, norm⟩)
Colors of variables: wff setvar class
This definition is referenced by:  axhilex-zf  28188  axhfvadd-zf  28189  axhvcom-zf  28190  axhvass-zf  28191  axhv0cl-zf  28192  axhvaddid-zf  28193  axhfvmul-zf  28194  axhvmulid-zf  28195  axhvmulass-zf  28196  axhvdistr1-zf  28197  axhvdistr2-zf  28198  axhvmul0-zf  28199  axhfi-zf  28200  axhis1-zf  28201  axhis2-zf  28202  axhis3-zf  28203  axhis4-zf  28204  axhcompl-zf  28205  bcsiHIL  28387  hlimadd  28400  hhssabloilem  28468  pjhthlem2  28601  nmopsetretHIL  29073  nmopub2tHIL  29119  hmopbdoptHIL  29197
  Copyright terms: Public domain W3C validator