Metamath Proof Explorer

Theorem rngoa4

Description: Obsolete theorem, use ringabl and ablcmn and cmn4 instead. Rearrangement of 4 terms in a sum of ring elements. (Contributed by Steve Rodriguez, 9-Sep-2007) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses ringgcl.1 ⊢ G = 1 st ⁡ R
ringgcl.2 ⊢ X = ran ⁡ G
Assertion rngoa4 ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → A G B G C G D = A G C G B G D

Proof

Step Hyp Ref Expression
1 ringgcl.1 ⊢ G = 1 st ⁡ R
2 ringgcl.2 ⊢ X = ran ⁡ G
3 1 rngoablo ⊢ R ∈ RingOps → G ∈ AbelOp
4 2 ablo4 ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → A G B G C G D = A G C G B G D
5 3 4 syl3an1 ⊢ R ∈ RingOps ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X ∧ D ∈ X → A G B G C G D = A G C G B G D