Theorem hv2negi

Description: Two ways to express the negative of a vector. (Contributed by NM, 31-Oct-1999) (New usage is discouraged.)

	Ref	Expression
Hypothesis	hvaddid2.1	$$⊢A\in \mathscr{H}$$
Assertion	hv2negi	$$⊢0_{ℎ}{-}_{ℎ}A=-1{\cdot }_{ℎ}A$$

Proof

Step	Hyp	Ref	Expression
1		hvaddid2.1	$$⊢A\in \mathscr{H}$$
2		hv2neg	$$⊢A\in \mathscr{H}\to 0_{ℎ}{-}_{ℎ}A=-1{\cdot }_{ℎ}A$$
3	1 2	ax-mp	$$⊢0_{ℎ}{-}_{ℎ}A=-1{\cdot }_{ℎ}A$$