# Metamath Proof Explorer

## Theorem ablodiv32

Description: Swap the second and third terms in a double division. (Contributed by NM, 29-Feb-2008) (New usage is discouraged.)

Ref Expression
Hypotheses abldiv.1 ${⊢}{X}=\mathrm{ran}{G}$
abldiv.3 ${⊢}{D}={/}_{g}\left({G}\right)$
Assertion ablodiv32 ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{D}{B}\right){D}{C}=\left({A}{D}{C}\right){D}{B}$

### Proof

Step Hyp Ref Expression
1 abldiv.1 ${⊢}{X}=\mathrm{ran}{G}$
2 abldiv.3 ${⊢}{D}={/}_{g}\left({G}\right)$
3 1 ablocom ${⊢}\left({G}\in \mathrm{AbelOp}\wedge {B}\in {X}\wedge {C}\in {X}\right)\to {B}{G}{C}={C}{G}{B}$
4 3 3adant3r1 ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to {B}{G}{C}={C}{G}{B}$
5 4 oveq2d ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to {A}{D}\left({B}{G}{C}\right)={A}{D}\left({C}{G}{B}\right)$
6 1 2 ablodivdiv4 ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{D}{B}\right){D}{C}={A}{D}\left({B}{G}{C}\right)$
7 3ancomb ${⊢}\left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)↔\left({A}\in {X}\wedge {C}\in {X}\wedge {B}\in {X}\right)$
8 1 2 ablodivdiv4 ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {C}\in {X}\wedge {B}\in {X}\right)\right)\to \left({A}{D}{C}\right){D}{B}={A}{D}\left({C}{G}{B}\right)$
9 7 8 sylan2b ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{D}{C}\right){D}{B}={A}{D}\left({C}{G}{B}\right)$
10 5 6 9 3eqtr4d ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{D}{B}\right){D}{C}=\left({A}{D}{C}\right){D}{B}$