Definition df-hba 27954

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 27984). 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 28152. (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		chil 27904	. 2 class ℋ
2		cva 27905	. . . . 5 class +ℎ
3		csm 27906	. . . . 5 class ·ℎ
4	2, 3	cop 4216	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 27908	. . . 4 class normℎ
6	4, 5	cop 4216	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cba 27569	. . 3 class BaseSet
8	6, 7	cfv 5926	. 2 class (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1523	1 wff ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhilex-zf  27966  axhfvadd-zf  27967  axhvcom-zf  27968  axhvass-zf  27969  axhv0cl-zf  27970  axhvaddid-zf  27971  axhfvmul-zf  27972  axhvmulid-zf  27973  axhvmulass-zf  27974  axhvdistr1-zf  27975  axhvdistr2-zf  27976  axhvmul0-zf  27977  axhfi-zf  27978  axhis1-zf  27979  axhis2-zf  27980  axhis3-zf  27981  axhis4-zf  27982  axhcompl-zf  27983  bcsiHIL  28165  hlimadd  28178  hhssabloilem  28246  pjhthlem2  28379  nmopsetretHIL  28851  nmopub2tHIL  28897  hmopbdoptHIL  28975