Definition df-hba 29340

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 29370). 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 29538. (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 29290	. 2 class ℋ
2		cva 29291	. . . . 5 class +ℎ
3		csm 29292	. . . . 5 class ·ℎ
4	2, 3	cop 4568	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 29294	. . . 4 class normℎ
6	4, 5	cop 4568	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cba 28957	. . 3 class BaseSet
8	6, 7	cfv 6437	. 2 class (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1539	1 wff ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhilex-zf  29352  axhfvadd-zf  29353  axhvcom-zf  29354  axhvass-zf  29355  axhv0cl-zf  29356  axhvaddid-zf  29357  axhfvmul-zf  29358  axhvmulid-zf  29359  axhvmulass-zf  29360  axhvdistr1-zf  29361  axhvdistr2-zf  29362  axhvmul0-zf  29363  axhfi-zf  29364  axhis1-zf  29365  axhis2-zf  29366  axhis3-zf  29367  axhis4-zf  29368  axhcompl-zf  29369  bcsiHIL  29551  hlimadd  29564  hhssabloilem  29632  pjhthlem2  29763  nmopsetretHIL  30235  nmopub2tHIL  30281  hmopbdoptHIL  30359