Definition df-hba 31058

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 31088). 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 31256. (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 31008	. 2 class ℋ
2		cva 31009	. . . . 5 class +ℎ
3		csm 31010	. . . . 5 class ·ℎ
4	2, 3	cop 4574	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 31012	. . . 4 class normℎ
6	4, 5	cop 4574	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cba 30675	. . 3 class BaseSet
8	6, 7	cfv 6493	. 2 class (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1542	1 wff ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhilex-zf  31070  axhfvadd-zf  31071  axhvcom-zf  31072  axhvass-zf  31073  axhv0cl-zf  31074  axhvaddid-zf  31075  axhfvmul-zf  31076  axhvmulid-zf  31077  axhvmulass-zf  31078  axhvdistr1-zf  31079  axhvdistr2-zf  31080  axhvmul0-zf  31081  axhfi-zf  31082  axhis1-zf  31083  axhis2-zf  31084  axhis3-zf  31085  axhis4-zf  31086  axhcompl-zf  31087  bcsiHIL  31269  hlimadd  31282  hhssabloilem  31350  pjhthlem2  31481  nmopsetretHIL  31953  nmopub2tHIL  31999  hmopbdoptHIL  32077