# Metamath Proof Explorer

## Theorem srgmgp

Description: A semiring is a monoid under multiplication. (Contributed by Thierry Arnoux, 21-Mar-2018)

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

### Proof

Step Hyp Ref Expression
1 srgmgp.g ${⊢}{G}={\mathrm{mulGrp}}_{{R}}$
2 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
3 eqid ${⊢}{+}_{{R}}={+}_{{R}}$
4 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
5 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
6 2 1 3 4 5 issrg ${⊢}{R}\in \mathrm{SRing}↔\left({R}\in \mathrm{CMnd}\wedge {G}\in \mathrm{Mnd}\wedge \forall {x}\in {\mathrm{Base}}_{{R}}\phantom{\rule{.4em}{0ex}}\left(\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)\wedge \left({0}_{{R}}{\cdot }_{{R}}{x}={0}_{{R}}\wedge {x}{\cdot }_{{R}}{0}_{{R}}={0}_{{R}}\right)\right)\right)$
7 6 simp2bi ${⊢}{R}\in \mathrm{SRing}\to {G}\in \mathrm{Mnd}$