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}\leftrightarrow \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)}\forall r\in {\mathrm{Base}}_{\mathrm{Scalar}\left(W\right)}\forall x\in {\mathrm{Base}}_W\forall w\in {\mathrm{Base}}_W\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}$$