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}\leftrightarrow \left(R\in \mathrm{Grp}\wedge G\in \mathrm{Mnd}\wedge \forall x\in {\mathrm{Base}}_R\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)\right)$$
6	5	simp2bi	$$⊢R\in \mathrm{Ring}\to G\in \mathrm{Mnd}$$