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	$$⊢\mathscr{H}=\mathrm{BaseSet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chba	$$class\mathscr{H}$$
1		cba	$$class\mathrm{BaseSet}$$
2		cva	$$class{+}_{ℎ}$$
3		csm	$$class{\cdot }_{ℎ}$$
4	2 3	cop	$$class⟨{+}_{ℎ},{\cdot }_{ℎ}⟩$$
5		cno	$$class{norm}_{ℎ}$$
6	4 5	cop	$$class⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
7	6 1	cfv	$$class\mathrm{BaseSet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
8	0 7	wceq	$$wff\mathscr{H}=\mathrm{BaseSet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$