Theorem hvsubid

Description: Subtraction of a vector from itself. (Contributed by NM, 30-May-1999) (New usage is discouraged.)

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

Proof

Step	Hyp	Ref	Expression
1		ax-hvmulid	$$⊢A\in \mathscr{H}\to 1{\cdot }_{ℎ}A=A$$
2	1	oveq1d	$$⊢A\in \mathscr{H}\to \left(1{\cdot }_{ℎ}A\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}A\right)=A{+}_{ℎ}\left(-1{\cdot }_{ℎ}A\right)$$
3		ax-1cn	$$⊢1\in ℂ$$
4		neg1cn	$$⊢-1\in ℂ$$
5		ax-hvdistr2	$$⊢\left(1\in ℂ\wedge -1\in ℂ\wedge A\in \mathscr{H}\right)\to \left(1+-1\right){\cdot }_{ℎ}A=\left(1{\cdot }_{ℎ}A\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}A\right)$$
6	3 4 5	mp3an12	$$⊢A\in \mathscr{H}\to \left(1+-1\right){\cdot }_{ℎ}A=\left(1{\cdot }_{ℎ}A\right){+}_{ℎ}\left(-1{\cdot }_{ℎ}A\right)$$
7		hvsubval	$$⊢\left(A\in \mathscr{H}\wedge A\in \mathscr{H}\right)\to A{-}_{ℎ}A=A{+}_{ℎ}\left(-1{\cdot }_{ℎ}A\right)$$
8	7	anidms	$$⊢A\in \mathscr{H}\to A{-}_{ℎ}A=A{+}_{ℎ}\left(-1{\cdot }_{ℎ}A\right)$$
9	2 6 8	3eqtr4rd	$$⊢A\in \mathscr{H}\to A{-}_{ℎ}A=\left(1+-1\right){\cdot }_{ℎ}A$$
10		1pneg1e0	$$⊢1+-1=0$$
11	10	oveq1i	$$⊢\left(1+-1\right){\cdot }_{ℎ}A=0{\cdot }_{ℎ}A$$
12	9 11	eqtrdi	$$⊢A\in \mathscr{H}\to A{-}_{ℎ}A=0{\cdot }_{ℎ}A$$
13		ax-hvmul0	$$⊢A\in \mathscr{H}\to 0{\cdot }_{ℎ}A=0_{ℎ}$$
14	12 13	eqtrd	$$⊢A\in \mathscr{H}\to A{-}_{ℎ}A=0_{ℎ}$$