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}\leftrightarrow \left(R\in \mathrm{CMnd}\wedge G\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	simp2bi	$$⊢R\in \mathrm{SRing}\to G\in \mathrm{Mnd}$$