Definition df-hba 28752

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 28782). 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 28950. (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 28702	. 2 class ℋ
2		cva 28703	. . . . 5 class +ℎ
3		csm 28704	. . . . 5 class ·ℎ
4	2, 3	cop 4531	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 28706	. . . 4 class normℎ
6	4, 5	cop 4531	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cba 28369	. . 3 class BaseSet
8	6, 7	cfv 6324	. 2 class (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1538	1 wff ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhilex-zf  28764  axhfvadd-zf  28765  axhvcom-zf  28766  axhvass-zf  28767  axhv0cl-zf  28768  axhvaddid-zf  28769  axhfvmul-zf  28770  axhvmulid-zf  28771  axhvmulass-zf  28772  axhvdistr1-zf  28773  axhvdistr2-zf  28774  axhvmul0-zf  28775  axhfi-zf  28776  axhis1-zf  28777  axhis2-zf  28778  axhis3-zf  28779  axhis4-zf  28780  axhcompl-zf  28781  bcsiHIL  28963  hlimadd  28976  hhssabloilem  29044  pjhthlem2  29175  nmopsetretHIL  29647  nmopub2tHIL  29693  hmopbdoptHIL  29771