Theorem hv2neg

Description: Two ways to express the negative of a vector. (Contributed by NM, 23-May-2005) (New usage is discouraged.)

	Ref	Expression
Assertion	hv2neg	$$⊢A\in \mathscr{H}\to 0_{ℎ}{-}_{ℎ}A=-1{\cdot }_{ℎ}A$$

Proof

Step	Hyp	Ref	Expression
1		ax-hv0cl	$$⊢0_{ℎ}\in \mathscr{H}$$
2		hvsubval	$$⊢\left(0_{ℎ}\in \mathscr{H}\wedge A\in \mathscr{H}\right)\to 0_{ℎ}{-}_{ℎ}A=0_{ℎ}{+}_{ℎ}\left(-1{\cdot }_{ℎ}A\right)$$
3	1 2	mpan	$$⊢A\in \mathscr{H}\to 0_{ℎ}{-}_{ℎ}A=0_{ℎ}{+}_{ℎ}\left(-1{\cdot }_{ℎ}A\right)$$
4		neg1cn	$$⊢-1\in ℂ$$
5		hvmulcl	$$⊢\left(-1\in ℂ\wedge A\in \mathscr{H}\right)\to -1{\cdot }_{ℎ}A\in \mathscr{H}$$
6	4 5	mpan	$$⊢A\in \mathscr{H}\to -1{\cdot }_{ℎ}A\in \mathscr{H}$$
7		hvaddlid	$$⊢-1{\cdot }_{ℎ}A\in \mathscr{H}\to 0_{ℎ}{+}_{ℎ}\left(-1{\cdot }_{ℎ}A\right)=-1{\cdot }_{ℎ}A$$
8	6 7	syl	$$⊢A\in \mathscr{H}\to 0_{ℎ}{+}_{ℎ}\left(-1{\cdot }_{ℎ}A\right)=-1{\cdot }_{ℎ}A$$
9	3 8	eqtrd	$$⊢A\in \mathscr{H}\to 0_{ℎ}{-}_{ℎ}A=-1{\cdot }_{ℎ}A$$