This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem hhva

Description: The group (addition) operation of Hilbert space. (Contributed by NM, 17-Nov-2007) (New usage is discouraged.)

		Ref	Expression
	Hypothesis	hhnv.1	$⊢ U = ⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩$
	Assertion	hhva	$⊢ +_{ℎ} = +_{v} (U)$

Step	Hyp	Ref	Expression
1		hhnv.1	$⊢ U = ⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩$
2	1	hhnv	$⊢ U \in NrmCVec$
3	1 2	h2hva	$⊢ +_{ℎ} = +_{v} (U)$