Definition df-hba 30949

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 30979). 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 31147. (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 30899	. 2 class ℋ
2		cva 30900	. . . . 5 class +ℎ
3		csm 30901	. . . . 5 class ·ℎ
4	2, 3	cop 4579	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 30903	. . . 4 class normℎ
6	4, 5	cop 4579	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cba 30566	. . 3 class BaseSet
8	6, 7	cfv 6481	. 2 class (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1541	1 wff ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhilex-zf  30961  axhfvadd-zf  30962  axhvcom-zf  30963  axhvass-zf  30964  axhv0cl-zf  30965  axhvaddid-zf  30966  axhfvmul-zf  30967  axhvmulid-zf  30968  axhvmulass-zf  30969  axhvdistr1-zf  30970  axhvdistr2-zf  30971  axhvmul0-zf  30972  axhfi-zf  30973  axhis1-zf  30974  axhis2-zf  30975  axhis3-zf  30976  axhis4-zf  30977  axhcompl-zf  30978  bcsiHIL  31160  hlimadd  31173  hhssabloilem  31241  pjhthlem2  31372  nmopsetretHIL  31844  nmopub2tHIL  31890  hmopbdoptHIL  31968