Definition df-hba 30905

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 30935). 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 31103. (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 30855	. 2 class ℋ
2		cva 30856	. . . . 5 class +ℎ
3		csm 30857	. . . . 5 class ·ℎ
4	2, 3	cop 4598	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 30859	. . . 4 class normℎ
6	4, 5	cop 4598	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cba 30522	. . 3 class BaseSet
8	6, 7	cfv 6514	. 2 class (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1540	1 wff ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhilex-zf  30917  axhfvadd-zf  30918  axhvcom-zf  30919  axhvass-zf  30920  axhv0cl-zf  30921  axhvaddid-zf  30922  axhfvmul-zf  30923  axhvmulid-zf  30924  axhvmulass-zf  30925  axhvdistr1-zf  30926  axhvdistr2-zf  30927  axhvmul0-zf  30928  axhfi-zf  30929  axhis1-zf  30930  axhis2-zf  30931  axhis3-zf  30932  axhis4-zf  30933  axhcompl-zf  30934  bcsiHIL  31116  hlimadd  31129  hhssabloilem  31197  pjhthlem2  31328  nmopsetretHIL  31800  nmopub2tHIL  31846  hmopbdoptHIL  31924