This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = {Base}_{W}$
	lmod4.p	$⊢ \underset{˙}{+} = +_{W}$
	lmodvaddsub4.m	$⊢ \underset{˙}{-} = -_{W}$
Assertion	lmodvpncan	$⊢ (W \in LMod \land A \in V \land B \in V) \to (A \underset{˙}{+} B) \underset{˙}{-} B = A$

Proof

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