Definition df-hba 30988

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 31018). 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 31186. (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 30938	. 2 class ℋ
2		cva 30939	. . . . 5 class +ℎ
3		csm 30940	. . . . 5 class ·ℎ
4	2, 3	cop 4632	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 30942	. . . 4 class normℎ
6	4, 5	cop 4632	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cba 30605	. . 3 class BaseSet
8	6, 7	cfv 6561	. 2 class (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1540	1 wff ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhilex-zf  31000  axhfvadd-zf  31001  axhvcom-zf  31002  axhvass-zf  31003  axhv0cl-zf  31004  axhvaddid-zf  31005  axhfvmul-zf  31006  axhvmulid-zf  31007  axhvmulass-zf  31008  axhvdistr1-zf  31009  axhvdistr2-zf  31010  axhvmul0-zf  31011  axhfi-zf  31012  axhis1-zf  31013  axhis2-zf  31014  axhis3-zf  31015  axhis4-zf  31016  axhcompl-zf  31017  bcsiHIL  31199  hlimadd  31212  hhssabloilem  31280  pjhthlem2  31411  nmopsetretHIL  31883  nmopub2tHIL  31929  hmopbdoptHIL  32007