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\left(U\right)$$

Proof

Step	Hyp	Ref	Expression
1		hhnv.1	$$⊢U=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
2	1	hhnv	$$⊢U\in \mathrm{NrmCVec}$$
3	1	hhba	$$⊢\mathscr{H}=\mathrm{BaseSet}\left(U\right)$$
4	1 2 3	h2hvs	$$⊢{-}_{ℎ}={-}_v\left(U\right)$$