Theorem rngmgp

Description: A non-unital ring is a semigroup under multiplication. (Contributed by AV, 17-Feb-2020)

	Ref	Expression
Hypothesis	rngmgp.g	$$⊢G={\mathrm{mulGrp}}_R$$
Assertion	rngmgp	$$⊢R\in \mathrm{Rng}\to G\in \mathrm{Smgrp}$$

Proof

Step	Hyp	Ref	Expression
1		rngmgp.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	isrng	$$⊢R\in \mathrm{Rng}\leftrightarrow \left(R\in \mathrm{Abel}\wedge G\in \mathrm{Smgrp}\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{Rng}\to G\in \mathrm{Smgrp}$$