Definition df-hba 30913

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 30943). 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 31111. (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 30863	. 2 class ℋ
2		cva 30864	. . . . 5 class +ℎ
3		csm 30865	. . . . 5 class ·ℎ
4	2, 3	cop 4583	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 30867	. . . 4 class normℎ
6	4, 5	cop 4583	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cba 30530	. . 3 class BaseSet
8	6, 7	cfv 6482	. 2 class (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1540	1 wff ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhilex-zf  30925  axhfvadd-zf  30926  axhvcom-zf  30927  axhvass-zf  30928  axhv0cl-zf  30929  axhvaddid-zf  30930  axhfvmul-zf  30931  axhvmulid-zf  30932  axhvmulass-zf  30933  axhvdistr1-zf  30934  axhvdistr2-zf  30935  axhvmul0-zf  30936  axhfi-zf  30937  axhis1-zf  30938  axhis2-zf  30939  axhis3-zf  30940  axhis4-zf  30941  axhcompl-zf  30942  bcsiHIL  31124  hlimadd  31137  hhssabloilem  31205  pjhthlem2  31336  nmopsetretHIL  31808  nmopub2tHIL  31854  hmopbdoptHIL  31932