Definition df-hba 31057

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 31087). 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 31255. (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 31007	. 2 class ℋ
2		cva 31008	. . . . 5 class +ℎ
3		csm 31009	. . . . 5 class ·ℎ
4	2, 3	cop 4588	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 31011	. . . 4 class normℎ
6	4, 5	cop 4588	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cba 30674	. . 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  31069  axhfvadd-zf  31070  axhvcom-zf  31071  axhvass-zf  31072  axhv0cl-zf  31073  axhvaddid-zf  31074  axhfvmul-zf  31075  axhvmulid-zf  31076  axhvmulass-zf  31077  axhvdistr1-zf  31078  axhvdistr2-zf  31079  axhvmul0-zf  31080  axhfi-zf  31081  axhis1-zf  31082  axhis2-zf  31083  axhis3-zf  31084  axhis4-zf  31085  axhcompl-zf  31086  bcsiHIL  31268  hlimadd  31281  hhssabloilem  31349  pjhthlem2  31480  nmopsetretHIL  31952  nmopub2tHIL  31998  hmopbdoptHIL  32076