# Metamath Proof Explorer

## Theorem rngoaass

Description: The addition operation of a ring is associative. (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 rngoaass ${⊢}\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}={A}{G}\left({B}{G}{C}\right)$

### Proof

Step Hyp Ref Expression
1 ringgcl.1 ${⊢}{G}={1}^{st}\left({R}\right)$
2 ringgcl.2 ${⊢}{X}=\mathrm{ran}{G}$
3 1 rngogrpo ${⊢}{R}\in \mathrm{RingOps}\to {G}\in \mathrm{GrpOp}$
4 2 grpoass ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{G}{B}\right){G}{C}={A}{G}\left({B}{G}{C}\right)$
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}={A}{G}\left({B}{G}{C}\right)$