Definition df-hba 31321

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 31351). 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 31519. (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 31271	. 2 class ℋ
2		cva 31272	. . . . 5 class +ℎ
3		csm 31273	. . . . 5 class ·ℎ
4	2, 3	cop 4595	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 31275	. . . 4 class normℎ
6	4, 5	cop 4595	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cba 30938	. . 3 class BaseSet
8	6, 7	cfv 6536	. 2 class (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1570	1 wff ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhilex-zf  31333  axhfvadd-zf  31334  axhvcom-zf  31335  axhvass-zf  31336  axhv0cl-zf  31337  axhvaddid-zf  31338  axhfvmul-zf  31339  axhvmulid-zf  31340  axhvmulass-zf  31341  axhvdistr1-zf  31342  axhvdistr2-zf  31343  axhvmul0-zf  31344  axhfi-zf  31345  axhis1-zf  31346  axhis2-zf  31347  axhis3-zf  31348  axhis4-zf  31349  axhcompl-zf  31350  bcsiHIL  31532  hlimadd  31545  hhssabloilem  31613  pjhthlem2  31744  nmopsetretHIL  32216  nmopub2tHIL  32262  hmopbdoptHIL  32340