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

Metamath Proof Explorer

Theorem hhvs

Description: The vector subtraction operation of Hilbert space. (Contributed by NM, 13-Dec-2007) (New usage is discouraged.)

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

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