Definition df-hba 29974

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 30004). 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 30172. (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 29924	. 2 class ℋ
2		cva 29925	. . . . 5 class +ℎ
3		csm 29926	. . . . 5 class ·ℎ
4	2, 3	cop 4597	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 29928	. . . 4 class normℎ
6	4, 5	cop 4597	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cba 29591	. . 3 class BaseSet
8	6, 7	cfv 6501	. 2 class (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1541	1 wff ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhilex-zf  29986  axhfvadd-zf  29987  axhvcom-zf  29988  axhvass-zf  29989  axhv0cl-zf  29990  axhvaddid-zf  29991  axhfvmul-zf  29992  axhvmulid-zf  29993  axhvmulass-zf  29994  axhvdistr1-zf  29995  axhvdistr2-zf  29996  axhvmul0-zf  29997  axhfi-zf  29998  axhis1-zf  29999  axhis2-zf  30000  axhis3-zf  30001  axhis4-zf  30002  axhcompl-zf  30003  bcsiHIL  30185  hlimadd  30198  hhssabloilem  30266  pjhthlem2  30397  nmopsetretHIL  30869  nmopub2tHIL  30915  hmopbdoptHIL  30993