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	⊢ 𝑉 = ( Base ‘ 𝑊 )
	lmodvnegid.p	⊢ + = ( +g ‘ 𝑊 )
	lmodvnegid.z	⊢ 0 = ( 0g ‘ 𝑊 )
	lmodvnegid.n	⊢ 𝑁 = ( invg ‘ 𝑊 )
Assertion	lmodvnegid	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 + ( 𝑁 ‘ 𝑋 ) ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		lmodvnegid.v	⊢ 𝑉 = ( Base ‘ 𝑊 )
2		lmodvnegid.p	⊢ + = ( +g ‘ 𝑊 )
3		lmodvnegid.z	⊢ 0 = ( 0g ‘ 𝑊 )
4		lmodvnegid.n	⊢ 𝑁 = ( invg ‘ 𝑊 )
5		lmodgrp	⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
6	1 2 3 4	grprinv	⊢ ( ( 𝑊 ∈ Grp ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 + ( 𝑁 ‘ 𝑋 ) ) = 0 )
7	5 6	sylan	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑋 ∈ 𝑉 ) → ( 𝑋 + ( 𝑁 ‘ 𝑋 ) ) = 0 )