Definition df-hba 31451

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 31481). 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 31649. (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 31401	. 2 class ℋ
2		cva 31402	. . . . 5 class +ℎ
3		csm 31403	. . . . 5 class ·ℎ
4	2, 3	cop 4590	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 31405	. . . 4 class normℎ
6	4, 5	cop 4590	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cba 31068	. . 3 class BaseSet
8	6, 7	cfv 6533	. 2 class (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1570	1 wff ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is used by:  axhilex-zf  31463  axhfvadd-zf  31464  axhvcom-zf  31465  axhvass-zf  31466  axhv0cl-zf  31467  axhvaddid-zf  31468  axhfvmul-zf  31469  axhvmulid-zf  31470  axhvmulass-zf  31471  axhvdistr1-zf  31472  axhvdistr2-zf  31473  axhvmul0-zf  31474  axhfi-zf  31475  axhis1-zf  31476  axhis2-zf  31477  axhis3-zf  31478  axhis4-zf  31479  axhcompl-zf  31480  bcsiHIL  31662  hlimadd  31675  hhssabloilem  31743  pjhthlem2  31874  nmopsetretHIL  32346  nmopub2tHIL  32392  hmopbdoptHIL  32470