Definition df-hba 28541

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 28571). 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 28739. (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 28491	. 2 class ℋ
2		cva 28492	. . . . 5 class +ℎ
3		csm 28493	. . . . 5 class ·ℎ
4	2, 3	cop 4442	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 28495	. . . 4 class normℎ
6	4, 5	cop 4442	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cba 28156	. . 3 class BaseSet
8	6, 7	cfv 6186	. 2 class (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1508	1 wff ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhilex-zf  28553  axhfvadd-zf  28554  axhvcom-zf  28555  axhvass-zf  28556  axhv0cl-zf  28557  axhvaddid-zf  28558  axhfvmul-zf  28559  axhvmulid-zf  28560  axhvmulass-zf  28561  axhvdistr1-zf  28562  axhvdistr2-zf  28563  axhvmul0-zf  28564  axhfi-zf  28565  axhis1-zf  28566  axhis2-zf  28567  axhis3-zf  28568  axhis4-zf  28569  axhcompl-zf  28570  bcsiHIL  28752  hlimadd  28765  hhssabloilem  28833  pjhthlem2  28966  nmopsetretHIL  29438  nmopub2tHIL  29484  hmopbdoptHIL  29562