Theorem lmodvpncan

Description: Addition/subtraction cancellation law for vectors. ( hvpncan analog.) (Contributed by NM, 16-Apr-2014) (Revised by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypotheses	lmod4.v	$$⊢V={\mathrm{Base}}_W$$
	lmod4.p	$$⊢\underset{\dot{}}{+}={+}_W$$
	lmodvaddsub4.m	$$⊢\underset{\dot{}}{-}={-}_W$$
Assertion	lmodvpncan	$$⊢\left(W\in \mathrm{LMod}\wedge A\in V\wedge B\in V\right)\to \left(A\underset{\dot{}}{+}B\right)\underset{\dot{}}{-}B=A$$

Proof

Step	Hyp	Ref	Expression
1		lmod4.v	$$⊢V={\mathrm{Base}}_W$$
2		lmod4.p	$$⊢\underset{\dot{}}{+}={+}_W$$
3		lmodvaddsub4.m	$$⊢\underset{\dot{}}{-}={-}_W$$
4		lmodgrp	$$⊢W\in \mathrm{LMod}\to W\in \mathrm{Grp}$$
5	1 2 3	grppncan	$$⊢\left(W\in \mathrm{Grp}\wedge A\in V\wedge B\in V\right)\to \left(A\underset{\dot{}}{+}B\right)\underset{\dot{}}{-}B=A$$
6	4 5	syl3an1	$$⊢\left(W\in \mathrm{LMod}\wedge A\in V\wedge B\in V\right)\to \left(A\underset{\dot{}}{+}B\right)\underset{\dot{}}{-}B=A$$