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}\leftrightarrow \left(R\in \mathrm{CMnd}\wedge {\mathrm{mulGrp}}_R\in \mathrm{Mnd}\wedge \forall x\in {\mathrm{Base}}_R\left(\forall y\in {\mathrm{Base}}_R\forall z\in {\mathrm{Base}}_R\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}$$