Definition df-hba 30851

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 30881). 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 31049. (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 30801	. 2 class ℋ
2		cva 30802	. . . . 5 class +ℎ
3		csm 30803	. . . . 5 class ·ℎ
4	2, 3	cop 4636	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 30805	. . . 4 class normℎ
6	4, 5	cop 4636	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cba 30468	. . 3 class BaseSet
8	6, 7	cfv 6549	. 2 class (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1533	1 wff ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhilex-zf  30863  axhfvadd-zf  30864  axhvcom-zf  30865  axhvass-zf  30866  axhv0cl-zf  30867  axhvaddid-zf  30868  axhfvmul-zf  30869  axhvmulid-zf  30870  axhvmulass-zf  30871  axhvdistr1-zf  30872  axhvdistr2-zf  30873  axhvmul0-zf  30874  axhfi-zf  30875  axhis1-zf  30876  axhis2-zf  30877  axhis3-zf  30878  axhis4-zf  30879  axhcompl-zf  30880  bcsiHIL  31062  hlimadd  31075  hhssabloilem  31143  pjhthlem2  31274  nmopsetretHIL  31746  nmopub2tHIL  31792  hmopbdoptHIL  31870