Definition df-hba 31261

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 31291). 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 31459. (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 31211	. 2 class ℋ
2		cva 31212	. . . . 5 class +ℎ
3		csm 31213	. . . . 5 class ·ℎ
4	2, 3	cop 4600	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 31215	. . . 4 class normℎ
6	4, 5	cop 4600	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cba 30878	. . 3 class BaseSet
8	6, 7	cfv 6537	. 2 class (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1567	1 wff ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhilex-zf  31273  axhfvadd-zf  31274  axhvcom-zf  31275  axhvass-zf  31276  axhv0cl-zf  31277  axhvaddid-zf  31278  axhfvmul-zf  31279  axhvmulid-zf  31280  axhvmulass-zf  31281  axhvdistr1-zf  31282  axhvdistr2-zf  31283  axhvmul0-zf  31284  axhfi-zf  31285  axhis1-zf  31286  axhis2-zf  31287  axhis3-zf  31288  axhis4-zf  31289  axhcompl-zf  31290  bcsiHIL  31472  hlimadd  31485  hhssabloilem  31553  pjhthlem2  31684  nmopsetretHIL  32156  nmopub2tHIL  32202  hmopbdoptHIL  32280