# Metamath Proof Explorer

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

### Detailed syntax breakdown

Step Hyp Ref Expression
0 chba ${class}ℋ$
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}ℋ=\mathrm{BaseSet}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$