Definition df-hba 30871

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 30901). 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 31069. (Contributed by NM, 31-May-2008.) (New usage is discouraged.)

Assertion

Ref	Expression
df-hba	⊢ ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

Detailed syntax breakdown of Definition df-hba

Step	Hyp	Ref	Expression
1		chba 30821	. 2 class ℋ
2		cva 30822	. . . . 5 class +ℎ
3		csm 30823	. . . . 5 class ·ℎ
4	2, 3	cop 4591	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 30825	. . . 4 class normℎ
6	4, 5	cop 4591	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cba 30488	. . 3 class BaseSet
8	6, 7	cfv 6499	. 2 class (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1540	1 wff ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhilex-zf  30883  axhfvadd-zf  30884  axhvcom-zf  30885  axhvass-zf  30886  axhv0cl-zf  30887  axhvaddid-zf  30888  axhfvmul-zf  30889  axhvmulid-zf  30890  axhvmulass-zf  30891  axhvdistr1-zf  30892  axhvdistr2-zf  30893  axhvmul0-zf  30894  axhfi-zf  30895  axhis1-zf  30896  axhis2-zf  30897  axhis3-zf  30898  axhis4-zf  30899  axhcompl-zf  30900  bcsiHIL  31082  hlimadd  31095  hhssabloilem  31163  pjhthlem2  31294  nmopsetretHIL  31766  nmopub2tHIL  31812  hmopbdoptHIL  31890