# Metamath Proof Explorer

## Theorem rngoa4

Description: Rearrangement of 4 terms in a sum of ring elements. (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 rngoa4 ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({A}\in {X}\wedge {B}\in {X}\right)\wedge \left({C}\in {X}\wedge {D}\in {X}\right)\right)\to \left({A}{G}{B}\right){G}\left({C}{G}{D}\right)=\left({A}{G}{C}\right){G}\left({B}{G}{D}\right)$

### 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 ablo4 ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\right)\wedge \left({C}\in {X}\wedge {D}\in {X}\right)\right)\to \left({A}{G}{B}\right){G}\left({C}{G}{D}\right)=\left({A}{G}{C}\right){G}\left({B}{G}{D}\right)$
5 3 4 syl3an1 ${⊢}\left({R}\in \mathrm{RingOps}\wedge \left({A}\in {X}\wedge {B}\in {X}\right)\wedge \left({C}\in {X}\wedge {D}\in {X}\right)\right)\to \left({A}{G}{B}\right){G}\left({C}{G}{D}\right)=\left({A}{G}{C}\right){G}\left({B}{G}{D}\right)$