# Metamath Proof Explorer

## Theorem ringmgp

Description: A ring is a monoid under multiplication. (Contributed by Mario Carneiro, 6-Jan-2015)

Ref Expression
Hypothesis ringmgp.g ${⊢}{G}={\mathrm{mulGrp}}_{{R}}$
Assertion ringmgp ${⊢}{R}\in \mathrm{Ring}\to {G}\in \mathrm{Mnd}$

### Proof

Step Hyp Ref Expression
1 ringmgp.g ${⊢}{G}={\mathrm{mulGrp}}_{{R}}$
2 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
3 eqid ${⊢}{+}_{{R}}={+}_{{R}}$
4 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
5 2 1 3 4 isring ${⊢}{R}\in \mathrm{Ring}↔\left({R}\in \mathrm{Grp}\wedge {G}\in \mathrm{Mnd}\wedge \forall {x}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\forall {y}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\forall {z}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\left({x}{\cdot }_{{R}}\left({y}{+}_{{R}}{z}\right)=\left({x}{\cdot }_{{R}}{y}\right){+}_{{R}}\left({x}{\cdot }_{{R}}{z}\right)\wedge \left({x}{+}_{{R}}{y}\right){\cdot }_{{R}}{z}=\left({x}{\cdot }_{{R}}{z}\right){+}_{{R}}\left({y}{\cdot }_{{R}}{z}\right)\right)\right)$
6 5 simp2bi ${⊢}{R}\in \mathrm{Ring}\to {G}\in \mathrm{Mnd}$