Theorem hvsubval

Description: Value of vector subtraction. (Contributed by NM, 5-Sep-1999) (Revised by Mario Carneiro, 23-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Assertion	hvsubval	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to A{-}_{ℎ}B=A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)$$

Proof

Step	Hyp	Ref	Expression
1		oveq1	$$⊢x=A\to x{+}_{ℎ}\left(-1{\cdot }_{ℎ}y\right)=A{+}_{ℎ}\left(-1{\cdot }_{ℎ}y\right)$$
2		oveq2	$$⊢y=B\to -1{\cdot }_{ℎ}y=-1{\cdot }_{ℎ}B$$
3	2	oveq2d	$$⊢y=B\to A{+}_{ℎ}\left(-1{\cdot }_{ℎ}y\right)=A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)$$
4		df-hvsub	$$⊢{-}_{ℎ}=\left(x\in \mathscr{H},y\in \mathscr{H}⟼x{+}_{ℎ}\left(-1{\cdot }_{ℎ}y\right)\right)$$
5		ovex	$$⊢A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)\in \mathrm{V}$$
6	1 3 4 5	ovmpo	$$⊢\left(A\in \mathscr{H}\wedge B\in \mathscr{H}\right)\to A{-}_{ℎ}B=A{+}_{ℎ}\left(-1{\cdot }_{ℎ}B\right)$$