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=ran⁡G
abldiv.3 ⊢D=/g⁡G
Assertion ablodiv32 ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X→ADBDC=ADCDB

Proof

Step Hyp Ref Expression
1 abldiv.1 ⊢X=ran⁡G
2 abldiv.3 ⊢D=/g⁡G
3 1 ablocom ⊢G∈AbelOp∧B∈X∧C∈X→BGC=CGB
4 3 3adant3r1 ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X→BGC=CGB
5 4 oveq2d ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X→ADBGC=ADCGB
6 1 2 ablodivdiv4 ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X→ADBDC=ADBGC
7 3ancomb ⊢A∈X∧B∈X∧C∈X↔A∈X∧C∈X∧B∈X
8 1 2 ablodivdiv4 ⊢G∈AbelOp∧A∈X∧C∈X∧B∈X→ADCDB=ADCGB
9 7 8 sylan2b ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X→ADCDB=ADCGB
10 5 6 9 3eqtr4d ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X→ADBDC=ADCDB