Metamath Proof Explorer

Theorem ablodivdiv

Description: Law for double group 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 ablodivdiv ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D B D C = A D B G C

Proof

Step Hyp Ref Expression
1 abldiv.1 ⊢ X = ran ⁡ G
2 abldiv.3 ⊢ D = / g ⁡ G
3 ablogrpo ⊢ G ∈ AbelOp → G ∈ GrpOp
4 1 2 grpodivdiv ⊢ G ∈ GrpOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D B D C = A G C D B
5 3 4 sylan ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D B D C = A G C D B
6 3ancomb ⊢ A ∈ X ∧ B ∈ X ∧ C ∈ X ↔ A ∈ X ∧ C ∈ X ∧ B ∈ X
7 1 2 grpomuldivass ⊢ G ∈ GrpOp ∧ A ∈ X ∧ C ∈ X ∧ B ∈ X → A G C D B = A G C D B
8 3 7 sylan ⊢ G ∈ AbelOp ∧ A ∈ X ∧ C ∈ X ∧ B ∈ X → A G C D B = A G C D B
9 1 2 ablomuldiv ⊢ G ∈ AbelOp ∧ A ∈ X ∧ C ∈ X ∧ B ∈ X → A G C D B = A D B G C
10 8 9 eqtr3d ⊢ G ∈ AbelOp ∧ A ∈ X ∧ C ∈ X ∧ B ∈ X → A G C D B = A D B G C
11 6 10 sylan2b ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A G C D B = A D B G C
12 5 11 eqtrd ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D B D C = A D B G C