Theorem lmodvnpcan

Description: Cancellation law for vector subtraction ( npcan analog). (Contributed by NM, 19-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	lmodvnpcan	$$⊢\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	grpnpcan	$$⊢\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$$