# Metamath Proof Explorer

## Theorem lmodring

Description: The scalar component of a left module is a ring. (Contributed by NM, 8-Dec-2013) (Revised by Mario Carneiro, 19-Jun-2014)

Ref Expression
Hypothesis lmodring.1 ${⊢}{F}=\mathrm{Scalar}\left({W}\right)$
Assertion lmodring ${⊢}{W}\in \mathrm{LMod}\to {F}\in \mathrm{Ring}$

### Proof

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