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	$$⊢W\in \mathrm{LMod}\to W\in \mathrm{Abel}$$

Proof

Step	Hyp	Ref	Expression
1		eqidd	$$⊢W\in \mathrm{LMod}\to {\mathrm{Base}}_W={\mathrm{Base}}_W$$
2		eqidd	$$⊢W\in \mathrm{LMod}\to {+}_W={+}_W$$
3		lmodgrp	$$⊢W\in \mathrm{LMod}\to W\in \mathrm{Grp}$$
4		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
5		eqid	$$⊢{+}_W={+}_W$$
6	4 5	lmodcom	$$⊢\left(W\in \mathrm{LMod}\wedge x\in {\mathrm{Base}}_W\wedge y\in {\mathrm{Base}}_W\right)\to x{+}_{W}y=y{+}_{W}x$$
7	1 2 3 6	isabld	$$⊢W\in \mathrm{LMod}\to W\in \mathrm{Abel}$$