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

Definition df-hba 27954
 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 27984). 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 28152. (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 27904 . 2 class
2 cva 27905 . . . . 5 class +
3 csm 27906 . . . . 5 class ·
42, 3cop 4216 . . . 4 class ⟨ + , ·
5 cno 27908 . . . 4 class norm
64, 5cop 4216 . . 3 class ⟨⟨ + , · ⟩, norm
7 cba 27569 . . 3 class BaseSet
86, 7cfv 5926 . 2 class (BaseSet‘⟨⟨ + , · ⟩, norm⟩)
91, 8wceq 1523 1 wff ℋ = (BaseSet‘⟨⟨ + , · ⟩, norm⟩)
 Colors of variables: wff setvar class This definition is referenced by:  axhilex-zf  27966  axhfvadd-zf  27967  axhvcom-zf  27968  axhvass-zf  27969  axhv0cl-zf  27970  axhvaddid-zf  27971  axhfvmul-zf  27972  axhvmulid-zf  27973  axhvmulass-zf  27974  axhvdistr1-zf  27975  axhvdistr2-zf  27976  axhvmul0-zf  27977  axhfi-zf  27978  axhis1-zf  27979  axhis2-zf  27980  axhis3-zf  27981  axhis4-zf  27982  axhcompl-zf  27983  bcsiHIL  28165  hlimadd  28178  hhssabloilem  28246  pjhthlem2  28379  nmopsetretHIL  28851  nmopub2tHIL  28897  hmopbdoptHIL  28975
 Copyright terms: Public domain W3C validator