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 30851
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 30881). 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 31049. (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 30801 . 2 class
2 cva 30802 . . . . 5 class +
3 csm 30803 . . . . 5 class ·
42, 3cop 4636 . . . 4 class ⟨ + , ·
5 cno 30805 . . . 4 class norm
64, 5cop 4636 . . 3 class ⟨⟨ + , · ⟩, norm
7 cba 30468 . . 3 class BaseSet
86, 7cfv 6549 . 2 class (BaseSet‘⟨⟨ + , · ⟩, norm⟩)
91, 8wceq 1533 1 wff ℋ = (BaseSet‘⟨⟨ + , · ⟩, norm⟩)
Colors of variables: wff setvar class
This definition is referenced by:  axhilex-zf  30863  axhfvadd-zf  30864  axhvcom-zf  30865  axhvass-zf  30866  axhv0cl-zf  30867  axhvaddid-zf  30868  axhfvmul-zf  30869  axhvmulid-zf  30870  axhvmulass-zf  30871  axhvdistr1-zf  30872  axhvdistr2-zf  30873  axhvmul0-zf  30874  axhfi-zf  30875  axhis1-zf  30876  axhis2-zf  30877  axhis3-zf  30878  axhis4-zf  30879  axhcompl-zf  30880  bcsiHIL  31062  hlimadd  31075  hhssabloilem  31143  pjhthlem2  31274  nmopsetretHIL  31746  nmopub2tHIL  31792  hmopbdoptHIL  31870
  Copyright terms: Public domain W3C validator