Definition df-hba 30993

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 31023). 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 31191. (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 30943	. 2 class ℋ
2		cva 30944	. . . . 5 class +ℎ
3		csm 30945	. . . . 5 class ·ℎ
4	2, 3	cop 4584	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 30947	. . . 4 class normℎ
6	4, 5	cop 4584	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cba 30610	. . 3 class BaseSet
8	6, 7	cfv 6490	. 2 class (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1541	1 wff ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhilex-zf  31005  axhfvadd-zf  31006  axhvcom-zf  31007  axhvass-zf  31008  axhv0cl-zf  31009  axhvaddid-zf  31010  axhfvmul-zf  31011  axhvmulid-zf  31012  axhvmulass-zf  31013  axhvdistr1-zf  31014  axhvdistr2-zf  31015  axhvmul0-zf  31016  axhfi-zf  31017  axhis1-zf  31018  axhis2-zf  31019  axhis3-zf  31020  axhis4-zf  31021  axhcompl-zf  31022  bcsiHIL  31204  hlimadd  31217  hhssabloilem  31285  pjhthlem2  31416  nmopsetretHIL  31888  nmopub2tHIL  31934  hmopbdoptHIL  32012