Definition df-hba

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 ). Note that ~H 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 . (Contributed by NM, 31-May-2008) (New usage is discouraged.)

	Ref	Expression
Assertion	df-hba	⊢ ℋ = ( BaseSet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chba	⊢ ℋ
1		cba	⊢ BaseSet
2		cva	⊢ +ℎ
3		csm	⊢ ·ℎ
4	2 3	cop	⊢ ⟨ +ℎ , ·ℎ ⟩
5		cno	⊢ normℎ
6	4 5	cop	⊢ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
7	6 1	cfv	⊢ ( BaseSet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
8	0 7	wceq	⊢ ℋ = ( BaseSet ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )