Definition df-hba 29232

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 29262). 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 29430. (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 29182	. 2 class ℋ
2		cva 29183	. . . . 5 class +ℎ
3		csm 29184	. . . . 5 class ·ℎ
4	2, 3	cop 4564	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 29186	. . . 4 class normℎ
6	4, 5	cop 4564	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cba 28849	. . 3 class BaseSet
8	6, 7	cfv 6418	. 2 class (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1539	1 wff ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhilex-zf  29244  axhfvadd-zf  29245  axhvcom-zf  29246  axhvass-zf  29247  axhv0cl-zf  29248  axhvaddid-zf  29249  axhfvmul-zf  29250  axhvmulid-zf  29251  axhvmulass-zf  29252  axhvdistr1-zf  29253  axhvdistr2-zf  29254  axhvmul0-zf  29255  axhfi-zf  29256  axhis1-zf  29257  axhis2-zf  29258  axhis3-zf  29259  axhis4-zf  29260  axhcompl-zf  29261  bcsiHIL  29443  hlimadd  29456  hhssabloilem  29524  pjhthlem2  29655  nmopsetretHIL  30127  nmopub2tHIL  30173  hmopbdoptHIL  30251