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 28541
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 28571). 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 28739. (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 28491 . 2 class
2 cva 28492 . . . . 5 class +
3 csm 28493 . . . . 5 class ·
42, 3cop 4442 . . . 4 class ⟨ + , ·
5 cno 28495 . . . 4 class norm
64, 5cop 4442 . . 3 class ⟨⟨ + , · ⟩, norm
7 cba 28156 . . 3 class BaseSet
86, 7cfv 6186 . 2 class (BaseSet‘⟨⟨ + , · ⟩, norm⟩)
91, 8wceq 1508 1 wff ℋ = (BaseSet‘⟨⟨ + , · ⟩, norm⟩)
Colors of variables: wff setvar class
This definition is referenced by:  axhilex-zf  28553  axhfvadd-zf  28554  axhvcom-zf  28555  axhvass-zf  28556  axhv0cl-zf  28557  axhvaddid-zf  28558  axhfvmul-zf  28559  axhvmulid-zf  28560  axhvmulass-zf  28561  axhvdistr1-zf  28562  axhvdistr2-zf  28563  axhvmul0-zf  28564  axhfi-zf  28565  axhis1-zf  28566  axhis2-zf  28567  axhis3-zf  28568  axhis4-zf  28569  axhcompl-zf  28570  bcsiHIL  28752  hlimadd  28765  hhssabloilem  28833  pjhthlem2  28966  nmopsetretHIL  29438  nmopub2tHIL  29484  hmopbdoptHIL  29562
  Copyright terms: Public domain W3C validator