Definition df-hba 30997

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 31027). 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 31195. (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 30947	. 2 class ℋ
2		cva 30948	. . . . 5 class +ℎ
3		csm 30949	. . . . 5 class ·ℎ
4	2, 3	cop 4636	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 30951	. . . 4 class normℎ
6	4, 5	cop 4636	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cba 30614	. . 3 class BaseSet
8	6, 7	cfv 6562	. 2 class (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1536	1 wff ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhilex-zf  31009  axhfvadd-zf  31010  axhvcom-zf  31011  axhvass-zf  31012  axhv0cl-zf  31013  axhvaddid-zf  31014  axhfvmul-zf  31015  axhvmulid-zf  31016  axhvmulass-zf  31017  axhvdistr1-zf  31018  axhvdistr2-zf  31019  axhvmul0-zf  31020  axhfi-zf  31021  axhis1-zf  31022  axhis2-zf  31023  axhis3-zf  31024  axhis4-zf  31025  axhcompl-zf  31026  bcsiHIL  31208  hlimadd  31221  hhssabloilem  31289  pjhthlem2  31420  nmopsetretHIL  31892  nmopub2tHIL  31938  hmopbdoptHIL  32016