Theorem lmodabl

Description: A left module is an abelian group (of vectors, under addition). (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 25-Jun-2014)

	Ref	Expression
Assertion	lmodabl	⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )

Proof

Step	Hyp	Ref	Expression
1		eqidd	⊢ ( 𝑊 ∈ LMod → ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 ) )
2		eqidd	⊢ ( 𝑊 ∈ LMod → ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 ) )
3		lmodgrp	⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
4		eqid	⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
5		eqid	⊢ ( +g ‘ 𝑊 ) = ( +g ‘ 𝑊 )
6	4 5	lmodcom	⊢ ( ( 𝑊 ∈ LMod ∧ 𝑥 ∈ ( Base ‘ 𝑊 ) ∧ 𝑦 ∈ ( Base ‘ 𝑊 ) ) → ( 𝑥 ( +g ‘ 𝑊 ) 𝑦 ) = ( 𝑦 ( +g ‘ 𝑊 ) 𝑥 ) )
7	1 2 3 6	isabld	⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Abel )