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 → A D B D C = A D C D B

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 → B G C = C G B
4 3 3adant3r1 ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → B G C = C G B
5 4 oveq2d ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D B G C = A D C G B
6 1 2 ablodivdiv4 ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D B D C = A D B G C
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 → A D C D B = A D C G B
9 7 8 sylan2b ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D C D B = A D C G B
10 5 6 9 3eqtr4d ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D B D C = A D C D B