# Metamath Proof Explorer

## Theorem rngoa32

Description: The addition operation of a ring is commutative. (Contributed by Steve Rodriguez, 9-Sep-2007) (New usage is discouraged.)

Ref Expression
Hypotheses ringgcl.1 ${⊢}{G}={1}^{st}\left({R}\right)$
ringgcl.2 ${⊢}{X}=\mathrm{ran}{G}$
Assertion rngoa32 ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{G}{B}\right){G}{C}=\left({A}{G}{C}\right){G}{B}$

### Proof

Step Hyp Ref Expression
1 ringgcl.1 ${⊢}{G}={1}^{st}\left({R}\right)$
2 ringgcl.2 ${⊢}{X}=\mathrm{ran}{G}$
3 1 rngoablo ${⊢}{R}\in \mathrm{RingOps}\to {G}\in \mathrm{AbelOp}$
4 2 ablo32 ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{G}{B}\right){G}{C}=\left({A}{G}{C}\right){G}{B}$
5 3 4 sylan ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{G}{B}\right){G}{C}=\left({A}{G}{C}\right){G}{B}$