Theorem rngabl

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

	Ref	Expression
Assertion	rngabl	|- ( R e. Rng -> R e. Abel )

Proof

Step	Hyp	Ref	Expression
1		eqid	|- ( Base ` R ) = ( Base ` R )
2		eqid	|- ( mulGrp ` R ) = ( mulGrp ` R )
3		eqid	|- ( +g ` R ) = ( +g ` R )
4		eqid	|- ( .r ` R ) = ( .r ` R )
5	1 2 3 4	isrng	|- ( R e. Rng <-> ( R e. Abel /\ ( mulGrp ` R ) e. Smgrp /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) A. z e. ( Base ` R ) ( ( x ( .r ` R ) ( y ( +g ` R ) z ) ) = ( ( x ( .r ` R ) y ) ( +g ` R ) ( x ( .r ` R ) z ) ) /\ ( ( x ( +g ` R ) y ) ( .r ` R ) z ) = ( ( x ( .r ` R ) z ) ( +g ` R ) ( y ( .r ` R ) z ) ) ) ) )
6	5	simp1bi	|- ( R e. Rng -> R e. Abel )