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

Metamath Proof Explorer

Theorem lmodvnegid

Description: Addition of a vector with its negative. (Contributed by NM, 18-Apr-2014) (Revised by Mario Carneiro, 19-Jun-2014)

	Ref	Expression
Hypotheses	lmodvnegid.v	$⊢ V = {Base}_{W}$
	lmodvnegid.p	$⊢ \underset{˙}{+} = +_{W}$
	lmodvnegid.z	$⊢ \underset{˙}{0} = 0_{W}$
	lmodvnegid.n	$⊢ N = {inv}_{g} (W)$
Assertion	lmodvnegid	$⊢ (W \in LMod \land X \in V) \to X \underset{˙}{+} N (X) = \underset{˙}{0}$

Step	Hyp	Ref	Expression
1		lmodvnegid.v	$⊢ V = {Base}_{W}$
2		lmodvnegid.p	$⊢ \underset{˙}{+} = +_{W}$
3		lmodvnegid.z	$⊢ \underset{˙}{0} = 0_{W}$
4		lmodvnegid.n	$⊢ N = {inv}_{g} (W)$
5		lmodgrp	$⊢ W \in LMod \to W \in Grp$
6	1 2 3 4	grprinv	$⊢ (W \in Grp \land X \in V) \to X \underset{˙}{+} N (X) = \underset{˙}{0}$
7	5 6	sylan	$⊢ (W \in LMod \land X \in V) \to X \underset{˙}{+} N (X) = \underset{˙}{0}$