Definition df-hba 27210

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 27240). 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 27408. (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		chil 27160	. 2 class ℋ
2		cva 27161	. . . . 5 class +ℎ
3		csm 27162	. . . . 5 class ·ℎ
4	2, 3	cop 4131	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 27164	. . . 4 class normℎ
6	4, 5	cop 4131	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cba 26825	. . 3 class BaseSet
8	6, 7	cfv 5804	. 2 class (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1475	1 wff ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhilex-zf  27222  axhfvadd-zf  27223  axhvcom-zf  27224  axhvass-zf  27225  axhv0cl-zf  27226  axhvaddid-zf  27227  axhfvmul-zf  27228  axhvmulid-zf  27229  axhvmulass-zf  27230  axhvdistr1-zf  27231  axhvdistr2-zf  27232  axhvmul0-zf  27233  axhfi-zf  27234  axhis1-zf  27235  axhis2-zf  27236  axhis3-zf  27237  axhis4-zf  27238  axhcompl-zf  27239  bcsiHIL  27421  hlimadd  27434  hhssabloilem  27502  pjhthlem2  27635  nmopsetretHIL  28107  nmopub2tHIL  28153  hmopbdoptHIL  28231