Definition df-hba 31169

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 31199). 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 31367. (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 31119	. 2 class ℋ
2		cva 31120	. . . . 5 class +ℎ
3		csm 31121	. . . . 5 class ·ℎ
4	2, 3	cop 4588	. . . 4 class ⟨ +ℎ , ·ℎ ⟩
5		cno 31123	. . . 4 class normℎ
6	4, 5	cop 4588	. . 3 class ⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩
7		cba 30786	. . 3 class BaseSet
8	6, 7	cfv 6521	. 2 class (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)
9	1, 8	wceq 1560	1 wff ℋ = (BaseSet‘⟨⟨ +ℎ , ·ℎ ⟩, normℎ⟩)

This definition is referenced by:  axhilex-zf  31181  axhfvadd-zf  31182  axhvcom-zf  31183  axhvass-zf  31184  axhv0cl-zf  31185  axhvaddid-zf  31186  axhfvmul-zf  31187  axhvmulid-zf  31188  axhvmulass-zf  31189  axhvdistr1-zf  31190  axhvdistr2-zf  31191  axhvmul0-zf  31192  axhfi-zf  31193  axhis1-zf  31194  axhis2-zf  31195  axhis3-zf  31196  axhis4-zf  31197  axhcompl-zf  31198  bcsiHIL  31380  hlimadd  31393  hhssabloilem  31461  pjhthlem2  31592  nmopsetretHIL  32064  nmopub2tHIL  32110  hmopbdoptHIL  32188