Definition df-hba 30898

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 30928). 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 31096. (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 30848	. 2 class ℋ
2		cva 30849	. . . . 5 class +ℎ
3		csm 30850	. . . . 5 class ·ℎ
4	2, 3	cop 4595	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 30852	. . . 4 class normℎ
6	4, 5	cop 4595	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cba 30515	. . 3 class BaseSet
8	6, 7	cfv 6511	. 2 class (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1540	1 wff ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhilex-zf  30910  axhfvadd-zf  30911  axhvcom-zf  30912  axhvass-zf  30913  axhv0cl-zf  30914  axhvaddid-zf  30915  axhfvmul-zf  30916  axhvmulid-zf  30917  axhvmulass-zf  30918  axhvdistr1-zf  30919  axhvdistr2-zf  30920  axhvmul0-zf  30921  axhfi-zf  30922  axhis1-zf  30923  axhis2-zf  30924  axhis3-zf  30925  axhis4-zf  30926  axhcompl-zf  30927  bcsiHIL  31109  hlimadd  31122  hhssabloilem  31190  pjhthlem2  31321  nmopsetretHIL  31793  nmopub2tHIL  31839  hmopbdoptHIL  31917