Definition df-hba 31001

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 31031). 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 31199. (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 30951	. 2 class ℋ
2		cva 30952	. . . . 5 class +ℎ
3		csm 30953	. . . . 5 class ·ℎ
4	2, 3	cop 4654	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 30955	. . . 4 class normℎ
6	4, 5	cop 4654	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cba 30618	. . 3 class BaseSet
8	6, 7	cfv 6573	. 2 class (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1537	1 wff ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhilex-zf  31013  axhfvadd-zf  31014  axhvcom-zf  31015  axhvass-zf  31016  axhv0cl-zf  31017  axhvaddid-zf  31018  axhfvmul-zf  31019  axhvmulid-zf  31020  axhvmulass-zf  31021  axhvdistr1-zf  31022  axhvdistr2-zf  31023  axhvmul0-zf  31024  axhfi-zf  31025  axhis1-zf  31026  axhis2-zf  31027  axhis3-zf  31028  axhis4-zf  31029  axhcompl-zf  31030  bcsiHIL  31212  hlimadd  31225  hhssabloilem  31293  pjhthlem2  31424  nmopsetretHIL  31896  nmopub2tHIL  31942  hmopbdoptHIL  32020