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	|- .+ = ( +g ` W )
	lmodvnegid.z	|- .0. = ( 0g ` W )
	lmodvnegid.n	|- N = ( invg ` W )
Assertion	lmodvnegid	|- ( ( W e. LMod /\ X e. V ) -> ( X .+ ( N ` X ) ) = .0. )

Proof

Step	Hyp	Ref	Expression
1		lmodvnegid.v	|- V = ( Base ` W )
2		lmodvnegid.p	|- .+ = ( +g ` W )
3		lmodvnegid.z	|- .0. = ( 0g ` W )
4		lmodvnegid.n	|- N = ( invg ` W )
5		lmodgrp	|- ( W e. LMod -> W e. Grp )
6	1 2 3 4	grprinv	|- ( ( W e. Grp /\ X e. V ) -> ( X .+ ( N ` X ) ) = .0. )
7	5 6	sylan	|- ( ( W e. LMod /\ X e. V ) -> ( X .+ ( N ` X ) ) = .0. )