Definition df-hba 31583

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 31613). 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 31781. (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 31533	. 2 class ℋ
2		cva 31534	. . . . 5 class +ℎ
3		csm 31535	. . . . 5 class ·ℎ
4	2, 3	cop 4837	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 31537	. . . 4 class normℎ
6	4, 5	cop 4837	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cba 31200	. . 3 class BaseSet
8	6, 7	cfv 6546	. 2 class (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1569	1 wff ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is used by:  axhilex-zf  31595  axhfvadd-zf  31596  axhvcom-zf  31597  axhvass-zf  31598  axhv0cl-zf  31599  axhvaddid-zf  31600  axhfvmul-zf  31601  axhvmulid-zf  31602  axhvmulass-zf  31603  axhvdistr1-zf  31604  axhvdistr2-zf  31605  axhvmul0-zf  31606  axhfi-zf  31607  axhis1-zf  31608  axhis2-zf  31609  axhis3-zf  31610  axhis4-zf  31611  axhcompl-zf  31612  bcsiHIL  31794  hlimadd  31807  hhssabloilem  31875  pjhthlem2  32006  nmopsetretHIL  32478  nmopub2tHIL  32524  hmopbdoptHIL  32602