Definition df-hba 30948

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 30978). 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 31146. (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 30898	. 2 class ℋ
2		cva 30899	. . . . 5 class +ℎ
3		csm 30900	. . . . 5 class ·ℎ
4	2, 3	cop 4591	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 30902	. . . 4 class normℎ
6	4, 5	cop 4591	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cba 30565	. . 3 class BaseSet
8	6, 7	cfv 6499	. 2 class (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1540	1 wff ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhilex-zf  30960  axhfvadd-zf  30961  axhvcom-zf  30962  axhvass-zf  30963  axhv0cl-zf  30964  axhvaddid-zf  30965  axhfvmul-zf  30966  axhvmulid-zf  30967  axhvmulass-zf  30968  axhvdistr1-zf  30969  axhvdistr2-zf  30970  axhvmul0-zf  30971  axhfi-zf  30972  axhis1-zf  30973  axhis2-zf  30974  axhis3-zf  30975  axhis4-zf  30976  axhcompl-zf  30977  bcsiHIL  31159  hlimadd  31172  hhssabloilem  31240  pjhthlem2  31371  nmopsetretHIL  31843  nmopub2tHIL  31889  hmopbdoptHIL  31967