Definition df-hba 31044

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 31074). 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 31242. (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 30994	. 2 class ℋ
2		cva 30995	. . . . 5 class +ℎ
3		csm 30996	. . . . 5 class ·ℎ
4	2, 3	cop 4586	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 30998	. . . 4 class normℎ
6	4, 5	cop 4586	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cba 30661	. . 3 class BaseSet
8	6, 7	cfv 6492	. 2 class (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1541	1 wff ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhilex-zf  31056  axhfvadd-zf  31057  axhvcom-zf  31058  axhvass-zf  31059  axhv0cl-zf  31060  axhvaddid-zf  31061  axhfvmul-zf  31062  axhvmulid-zf  31063  axhvmulass-zf  31064  axhvdistr1-zf  31065  axhvdistr2-zf  31066  axhvmul0-zf  31067  axhfi-zf  31068  axhis1-zf  31069  axhis2-zf  31070  axhis3-zf  31071  axhis4-zf  31072  axhcompl-zf  31073  bcsiHIL  31255  hlimadd  31268  hhssabloilem  31336  pjhthlem2  31467  nmopsetretHIL  31939  nmopub2tHIL  31985  hmopbdoptHIL  32063