Definition df-hba 30896

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 30926). 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 31094. (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 30846	. 2 class ℋ
2		cva 30847	. . . . 5 class +ℎ
3		csm 30848	. . . . 5 class ·ℎ
4	2, 3	cop 4607	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 30850	. . . 4 class normℎ
6	4, 5	cop 4607	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cba 30513	. . 3 class BaseSet
8	6, 7	cfv 6530	. 2 class (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1540	1 wff ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhilex-zf  30908  axhfvadd-zf  30909  axhvcom-zf  30910  axhvass-zf  30911  axhv0cl-zf  30912  axhvaddid-zf  30913  axhfvmul-zf  30914  axhvmulid-zf  30915  axhvmulass-zf  30916  axhvdistr1-zf  30917  axhvdistr2-zf  30918  axhvmul0-zf  30919  axhfi-zf  30920  axhis1-zf  30921  axhis2-zf  30922  axhis3-zf  30923  axhis4-zf  30924  axhcompl-zf  30925  bcsiHIL  31107  hlimadd  31120  hhssabloilem  31188  pjhthlem2  31319  nmopsetretHIL  31791  nmopub2tHIL  31837  hmopbdoptHIL  31915