# Metamath Proof Explorer

## Theorem srgcmn

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

Ref Expression
Assertion srgcmn ${⊢}{R}\in \mathrm{SRing}\to {R}\in \mathrm{CMnd}$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
2 eqid ${⊢}{\mathrm{mulGrp}}_{{R}}={\mathrm{mulGrp}}_{{R}}$
3 eqid ${⊢}{+}_{{R}}={+}_{{R}}$
4 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
5 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
6 1 2 3 4 5 issrg ${⊢}{R}\in \mathrm{SRing}↔\left({R}\in \mathrm{CMnd}\wedge {\mathrm{mulGrp}}_{{R}}\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 simp1bi ${⊢}{R}\in \mathrm{SRing}\to {R}\in \mathrm{CMnd}$