Definition df-hba 28740

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 28770). 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 28938. (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 28690	. 2 class ℋ
2		cva 28691	. . . . 5 class +ℎ
3		csm 28692	. . . . 5 class ·ℎ
4	2, 3	cop 4566	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 28694	. . . 4 class normℎ
6	4, 5	cop 4566	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cba 28357	. . 3 class BaseSet
8	6, 7	cfv 6349	. 2 class (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1533	1 wff ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhilex-zf  28752  axhfvadd-zf  28753  axhvcom-zf  28754  axhvass-zf  28755  axhv0cl-zf  28756  axhvaddid-zf  28757  axhfvmul-zf  28758  axhvmulid-zf  28759  axhvmulass-zf  28760  axhvdistr1-zf  28761  axhvdistr2-zf  28762  axhvmul0-zf  28763  axhfi-zf  28764  axhis1-zf  28765  axhis2-zf  28766  axhis3-zf  28767  axhis4-zf  28768  axhcompl-zf  28769  bcsiHIL  28951  hlimadd  28964  hhssabloilem  29032  pjhthlem2  29163  nmopsetretHIL  29635  nmopub2tHIL  29681  hmopbdoptHIL  29759