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

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}{\mathrm{Base}}_{{W}}={\mathrm{Base}}_{{W}}$
2 eqid ${⊢}{+}_{{W}}={+}_{{W}}$
3 eqid ${⊢}{\cdot }_{{W}}={\cdot }_{{W}}$
4 eqid ${⊢}\mathrm{Scalar}\left({W}\right)=\mathrm{Scalar}\left({W}\right)$
5 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}$
6 eqid ${⊢}{+}_{\mathrm{Scalar}\left({W}\right)}={+}_{\mathrm{Scalar}\left({W}\right)}$
7 eqid ${⊢}{\cdot }_{\mathrm{Scalar}\left({W}\right)}={\cdot }_{\mathrm{Scalar}\left({W}\right)}$
8 eqid ${⊢}{1}_{\mathrm{Scalar}\left({W}\right)}={1}_{\mathrm{Scalar}\left({W}\right)}$
9 1 2 3 4 5 6 7 8 islmod ${⊢}{W}\in \mathrm{LMod}↔\left({W}\in \mathrm{Grp}\wedge \mathrm{Scalar}\left({W}\right)\in \mathrm{Ring}\wedge \forall {q}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\phantom{\rule{.4em}{0ex}}\forall {r}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({W}\right)}\phantom{\rule{.4em}{0ex}}\forall {x}\in {\mathrm{Base}}_{{W}}\phantom{\rule{.4em}{0ex}}\forall {w}\in {\mathrm{Base}}_{{W}}\phantom{\rule{.4em}{0ex}}\left(\left({r}{\cdot }_{{W}}{w}\in {\mathrm{Base}}_{{W}}\wedge {r}{\cdot }_{{W}}\left({w}{+}_{{W}}{x}\right)=\left({r}{\cdot }_{{W}}{w}\right){+}_{{W}}\left({r}{\cdot }_{{W}}{x}\right)\wedge \left({q}{+}_{\mathrm{Scalar}\left({W}\right)}{r}\right){\cdot }_{{W}}{w}=\left({q}{\cdot }_{{W}}{w}\right){+}_{{W}}\left({r}{\cdot }_{{W}}{w}\right)\right)\wedge \left(\left({q}{\cdot }_{\mathrm{Scalar}\left({W}\right)}{r}\right){\cdot }_{{W}}{w}={q}{\cdot }_{{W}}\left({r}{\cdot }_{{W}}{w}\right)\wedge {1}_{\mathrm{Scalar}\left({W}\right)}{\cdot }_{{W}}{w}={w}\right)\right)\right)$
10 9 simp1bi ${⊢}{W}\in \mathrm{LMod}\to {W}\in \mathrm{Grp}$