# Metamath Proof Explorer

## Theorem rngoablo

Description: A ring's addition operation is an Abelian group operation. (Contributed by Steve Rodriguez, 9-Sep-2007) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

Ref Expression
Hypothesis ringabl.1 ${⊢}{G}={1}^{st}\left({R}\right)$
Assertion rngoablo ${⊢}{R}\in \mathrm{RingOps}\to {G}\in \mathrm{AbelOp}$

### Proof

Step Hyp Ref Expression
1 ringabl.1 ${⊢}{G}={1}^{st}\left({R}\right)$
2 eqid ${⊢}{2}^{nd}\left({R}\right)={2}^{nd}\left({R}\right)$
3 eqid ${⊢}\mathrm{ran}{G}=\mathrm{ran}{G}$
4 1 2 3 rngoi ${⊢}{R}\in \mathrm{RingOps}\to \left(\left({G}\in \mathrm{AbelOp}\wedge {2}^{nd}\left({R}\right):\mathrm{ran}{G}×\mathrm{ran}{G}⟶\mathrm{ran}{G}\right)\wedge \left(\forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {z}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left(\left({x}{2}^{nd}\left({R}\right){y}\right){2}^{nd}\left({R}\right){z}={x}{2}^{nd}\left({R}\right)\left({y}{2}^{nd}\left({R}\right){z}\right)\wedge {x}{2}^{nd}\left({R}\right)\left({y}{G}{z}\right)=\left({x}{2}^{nd}\left({R}\right){y}\right){G}\left({x}{2}^{nd}\left({R}\right){z}\right)\wedge \left({x}{G}{y}\right){2}^{nd}\left({R}\right){z}=\left({x}{2}^{nd}\left({R}\right){z}\right){G}\left({y}{2}^{nd}\left({R}\right){z}\right)\right)\wedge \exists {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\left({x}{2}^{nd}\left({R}\right){y}={y}\wedge {y}{2}^{nd}\left({R}\right){x}={y}\right)\right)\right)$
5 4 simplld ${⊢}{R}\in \mathrm{RingOps}\to {G}\in \mathrm{AbelOp}$