Metamath Proof Explorer


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 WLModWAbel

Proof

Step Hyp Ref Expression
1 eqidd WLModBaseW=BaseW
2 eqidd WLMod+W=+W
3 lmodgrp WLModWGrp
4 eqid BaseW=BaseW
5 eqid +W=+W
6 4 5 lmodcom WLModxBaseWyBaseWx+Wy=y+Wx
7 1 2 3 6 isabld WLModWAbel