Definition df-hba 31040

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 31070). 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 31238. (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 30990	. 2 class ℋ
2		cva 30991	. . . . 5 class +ℎ
3		csm 30992	. . . . 5 class ·ℎ
4	2, 3	cop 4573	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 30994	. . . 4 class normℎ
6	4, 5	cop 4573	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cba 30657	. . 3 class BaseSet
8	6, 7	cfv 6498	. 2 class (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1542	1 wff ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhilex-zf  31052  axhfvadd-zf  31053  axhvcom-zf  31054  axhvass-zf  31055  axhv0cl-zf  31056  axhvaddid-zf  31057  axhfvmul-zf  31058  axhvmulid-zf  31059  axhvmulass-zf  31060  axhvdistr1-zf  31061  axhvdistr2-zf  31062  axhvmul0-zf  31063  axhfi-zf  31064  axhis1-zf  31065  axhis2-zf  31066  axhis3-zf  31067  axhis4-zf  31068  axhcompl-zf  31069  bcsiHIL  31251  hlimadd  31264  hhssabloilem  31332  pjhthlem2  31463  nmopsetretHIL  31935  nmopub2tHIL  31981  hmopbdoptHIL  32059