Definition df-hba 31571

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 31601). 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 31769. (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 31521	. 2 class ℋ
2		cva 31522	. . . . 5 class +ℎ
3		csm 31523	. . . . 5 class ·ℎ
4	2, 3	cop 4590	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 31525	. . . 4 class normℎ
6	4, 5	cop 4590	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cba 31188	. . 3 class BaseSet
8	6, 7	cfv 6538	. 2 class (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1570	1 wff ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is used by:  axhilex-zf  31583  axhfvadd-zf  31584  axhvcom-zf  31585  axhvass-zf  31586  axhv0cl-zf  31587  axhvaddid-zf  31588  axhfvmul-zf  31589  axhvmulid-zf  31590  axhvmulass-zf  31591  axhvdistr1-zf  31592  axhvdistr2-zf  31593  axhvmul0-zf  31594  axhfi-zf  31595  axhis1-zf  31596  axhis2-zf  31597  axhis3-zf  31598  axhis4-zf  31599  axhcompl-zf  31600  bcsiHIL  31782  hlimadd  31795  hhssabloilem  31863  pjhthlem2  31994  nmopsetretHIL  32466  nmopub2tHIL  32512  hmopbdoptHIL  32590