Definition df-hba 28746

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 28776). 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 28944. (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 28696	. 2 class ℋ
2		cva 28697	. . . . 5 class +ℎ
3		csm 28698	. . . . 5 class ·ℎ
4	2, 3	cop 4573	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 28700	. . . 4 class normℎ
6	4, 5	cop 4573	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cba 28363	. . 3 class BaseSet
8	6, 7	cfv 6355	. 2 class (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1537	1 wff ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhilex-zf  28758  axhfvadd-zf  28759  axhvcom-zf  28760  axhvass-zf  28761  axhv0cl-zf  28762  axhvaddid-zf  28763  axhfvmul-zf  28764  axhvmulid-zf  28765  axhvmulass-zf  28766  axhvdistr1-zf  28767  axhvdistr2-zf  28768  axhvmul0-zf  28769  axhfi-zf  28770  axhis1-zf  28771  axhis2-zf  28772  axhis3-zf  28773  axhis4-zf  28774  axhcompl-zf  28775  bcsiHIL  28957  hlimadd  28970  hhssabloilem  29038  pjhthlem2  29169  nmopsetretHIL  29641  nmopub2tHIL  29687  hmopbdoptHIL  29765