Definition df-hba 28176

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 28206). 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 28374. (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 28126	. 2 class ℋ
2		cva 28127	. . . . 5 class +ℎ
3		csm 28128	. . . . 5 class ·ℎ
4	2, 3	cop 4387	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 28130	. . . 4 class normℎ
6	4, 5	cop 4387	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cba 27791	. . 3 class BaseSet
8	6, 7	cfv 6110	. 2 class (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1637	1 wff ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhilex-zf  28188  axhfvadd-zf  28189  axhvcom-zf  28190  axhvass-zf  28191  axhv0cl-zf  28192  axhvaddid-zf  28193  axhfvmul-zf  28194  axhvmulid-zf  28195  axhvmulass-zf  28196  axhvdistr1-zf  28197  axhvdistr2-zf  28198  axhvmul0-zf  28199  axhfi-zf  28200  axhis1-zf  28201  axhis2-zf  28202  axhis3-zf  28203  axhis4-zf  28204  axhcompl-zf  28205  bcsiHIL  28387  hlimadd  28400  hhssabloilem  28468  pjhthlem2  28601  nmopsetretHIL  29073  nmopub2tHIL  29119  hmopbdoptHIL  29197