Theorem hvsub0

Description: Subtraction of a zero vector. (Contributed by NM, 2-Apr-2000) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		ax-hv0cl	$$⊢0_{ℎ}\in \mathscr{H}$$
2		hvsubval	$$⊢\left(A\in \mathscr{H}\wedge 0_{ℎ}\in \mathscr{H}\right)\to A{-}_{ℎ}{0}_{ℎ}=A{+}_{ℎ}\left(-1{\cdot }_{ℎ}{0}_{ℎ}\right)$$
3	1 2	mpan2	$$⊢A\in \mathscr{H}\to A{-}_{ℎ}{0}_{ℎ}=A{+}_{ℎ}\left(-1{\cdot }_{ℎ}{0}_{ℎ}\right)$$
4		neg1cn	$$⊢-1\in ℂ$$
5		hvmul0	$$⊢-1\in ℂ\to -1{\cdot }_{ℎ}{0}_{ℎ}=0_{ℎ}$$
6	4 5	ax-mp	$$⊢-1{\cdot }_{ℎ}{0}_{ℎ}=0_{ℎ}$$
7	6	oveq2i	$$⊢A{+}_{ℎ}\left(-1{\cdot }_{ℎ}{0}_{ℎ}\right)=A{+}_{ℎ}{0}_{ℎ}$$
8	3 7	eqtrdi	$$⊢A\in \mathscr{H}\to A{-}_{ℎ}{0}_{ℎ}=A{+}_{ℎ}{0}_{ℎ}$$
9		ax-hvaddid	$$⊢A\in \mathscr{H}\to A{+}_{ℎ}{0}_{ℎ}=A$$
10	8 9	eqtrd	$$⊢A\in \mathscr{H}\to A{-}_{ℎ}{0}_{ℎ}=A$$