Definition df-hba 30222

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 30252). 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 30420. (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 30172	. 2 class ℋ
2		cva 30173	. . . . 5 class +ℎ
3		csm 30174	. . . . 5 class ·ℎ
4	2, 3	cop 4635	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 30176	. . . 4 class normℎ
6	4, 5	cop 4635	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cba 29839	. . 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  30234  axhfvadd-zf  30235  axhvcom-zf  30236  axhvass-zf  30237  axhv0cl-zf  30238  axhvaddid-zf  30239  axhfvmul-zf  30240  axhvmulid-zf  30241  axhvmulass-zf  30242  axhvdistr1-zf  30243  axhvdistr2-zf  30244  axhvmul0-zf  30245  axhfi-zf  30246  axhis1-zf  30247  axhis2-zf  30248  axhis3-zf  30249  axhis4-zf  30250  axhcompl-zf  30251  bcsiHIL  30433  hlimadd  30446  hhssabloilem  30514  pjhthlem2  30645  nmopsetretHIL  31117  nmopub2tHIL  31163  hmopbdoptHIL  31241