Theorem rngabl

Description: A non-unital ring is an (additive) abelian group. (Contributed by AV, 17-Feb-2020)

	Ref	Expression
Assertion	rngabl	$$⊢R\in \mathrm{Rng}\to R\in \mathrm{Abel}$$

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	1 2 3 4	isrng	$$⊢R\in \mathrm{Rng}\leftrightarrow \left(R\in \mathrm{Abel}\wedge {\mathrm{mulGrp}}_R\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	simp1bi	$$⊢R\in \mathrm{Rng}\to R\in \mathrm{Abel}$$