Definition df-hba 30253

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 30283). 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 30451. (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 30203	. 2 class ℋ
2		cva 30204	. . . . 5 class +ℎ
3		csm 30205	. . . . 5 class ·ℎ
4	2, 3	cop 4635	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 30207	. . . 4 class normℎ
6	4, 5	cop 4635	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cba 29870	. . 3 class BaseSet
8	6, 7	cfv 6544	. 2 class (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1542	1 wff ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhilex-zf  30265  axhfvadd-zf  30266  axhvcom-zf  30267  axhvass-zf  30268  axhv0cl-zf  30269  axhvaddid-zf  30270  axhfvmul-zf  30271  axhvmulid-zf  30272  axhvmulass-zf  30273  axhvdistr1-zf  30274  axhvdistr2-zf  30275  axhvmul0-zf  30276  axhfi-zf  30277  axhis1-zf  30278  axhis2-zf  30279  axhis3-zf  30280  axhis4-zf  30281  axhcompl-zf  30282  bcsiHIL  30464  hlimadd  30477  hhssabloilem  30545  pjhthlem2  30676  nmopsetretHIL  31148  nmopub2tHIL  31194  hmopbdoptHIL  31272