Definition df-hba 31042

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 31072). 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 31240. (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 30992	. 2 class ℋ
2		cva 30993	. . . . 5 class +ℎ
3		csm 30994	. . . . 5 class ·ℎ
4	2, 3	cop 4574	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 30996	. . . 4 class normℎ
6	4, 5	cop 4574	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cba 30659	. . 3 class BaseSet
8	6, 7	cfv 6500	. 2 class (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1542	1 wff ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhilex-zf  31054  axhfvadd-zf  31055  axhvcom-zf  31056  axhvass-zf  31057  axhv0cl-zf  31058  axhvaddid-zf  31059  axhfvmul-zf  31060  axhvmulid-zf  31061  axhvmulass-zf  31062  axhvdistr1-zf  31063  axhvdistr2-zf  31064  axhvmul0-zf  31065  axhfi-zf  31066  axhis1-zf  31067  axhis2-zf  31068  axhis3-zf  31069  axhis4-zf  31070  axhcompl-zf  31071  bcsiHIL  31253  hlimadd  31266  hhssabloilem  31334  pjhthlem2  31465  nmopsetretHIL  31937  nmopub2tHIL  31983  hmopbdoptHIL  32061