Definition df-hba 31392

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 31422). 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 31590. (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 31342	. 2 class ℋ
2		cva 31343	. . . . 5 class +ℎ
3		csm 31344	. . . . 5 class ·ℎ
4	2, 3	cop 4597	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 31346	. . . 4 class normℎ
6	4, 5	cop 4597	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cba 31009	. . 3 class BaseSet
8	6, 7	cfv 6540	. 2 class (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1570	1 wff ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is used by:  axhilex-zf  31404  axhfvadd-zf  31405  axhvcom-zf  31406  axhvass-zf  31407  axhv0cl-zf  31408  axhvaddid-zf  31409  axhfvmul-zf  31410  axhvmulid-zf  31411  axhvmulass-zf  31412  axhvdistr1-zf  31413  axhvdistr2-zf  31414  axhvmul0-zf  31415  axhfi-zf  31416  axhis1-zf  31417  axhis2-zf  31418  axhis3-zf  31419  axhis4-zf  31420  axhcompl-zf  31421  bcsiHIL  31603  hlimadd  31616  hhssabloilem  31684  pjhthlem2  31815  nmopsetretHIL  32287  nmopub2tHIL  32333  hmopbdoptHIL  32411