Metamath Proof Explorer


Theorem lmodgrp

Description: A left module is a group. (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 25-Jun-2014)

Ref Expression
Assertion lmodgrp W LMod W Grp

Proof

Step Hyp Ref Expression
1 eqid Base W = Base W
2 eqid + W = + W
3 eqid W = W
4 eqid Scalar W = Scalar W
5 eqid Base Scalar W = Base Scalar W
6 eqid + Scalar W = + Scalar W
7 eqid Scalar W = Scalar W
8 eqid 1 Scalar W = 1 Scalar W
9 1 2 3 4 5 6 7 8 islmod W LMod W Grp Scalar W Ring q Base Scalar W r Base Scalar W x Base W w Base W r W w Base W r W w + W x = r W w + W r W x q + Scalar W r W w = q W w + W r W w q Scalar W r W w = q W r W w 1 Scalar W W w = w
10 9 simp1bi W LMod W Grp