# Metamath Proof Explorer

## Theorem rlmlmod

Description: The ring module is a module. (Contributed by Stefan O'Rear, 6-Dec-2014)

Ref Expression
Assertion rlmlmod ${⊢}{R}\in \mathrm{Ring}\to \mathrm{ringLMod}\left({R}\right)\in \mathrm{LMod}$

### Proof

Step Hyp Ref Expression
1 rlmval ${⊢}\mathrm{ringLMod}\left({R}\right)=\mathrm{subringAlg}\left({R}\right)\left({\mathrm{Base}}_{{R}}\right)$
2 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
3 2 subrgid ${⊢}{R}\in \mathrm{Ring}\to {\mathrm{Base}}_{{R}}\in \mathrm{SubRing}\left({R}\right)$
4 eqid ${⊢}\mathrm{subringAlg}\left({R}\right)\left({\mathrm{Base}}_{{R}}\right)=\mathrm{subringAlg}\left({R}\right)\left({\mathrm{Base}}_{{R}}\right)$
5 4 sralmod ${⊢}{\mathrm{Base}}_{{R}}\in \mathrm{SubRing}\left({R}\right)\to \mathrm{subringAlg}\left({R}\right)\left({\mathrm{Base}}_{{R}}\right)\in \mathrm{LMod}$
6 3 5 syl ${⊢}{R}\in \mathrm{Ring}\to \mathrm{subringAlg}\left({R}\right)\left({\mathrm{Base}}_{{R}}\right)\in \mathrm{LMod}$
7 1 6 eqeltrid ${⊢}{R}\in \mathrm{Ring}\to \mathrm{ringLMod}\left({R}\right)\in \mathrm{LMod}$