Metamath Proof Explorer

Theorem ablonnncan1

Description: Cancellation law for group division. ( nnncan1 analog.) (Contributed by NM, 7-Mar-2008) (New usage is discouraged.)

Ref Expression
Hypotheses abldiv.1 ⊢ X = ran ⁡ G
abldiv.3 ⊢ D = / g ⁡ G
Assertion ablonnncan1 ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D B D A D C = C D B

Proof

Step Hyp Ref Expression
1 abldiv.1 ⊢ X = ran ⁡ G
2 abldiv.3 ⊢ D = / g ⁡ G
3 simpr1 ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A ∈ X
4 simpr2 ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → B ∈ X
5 ablogrpo ⊢ G ∈ AbelOp → G ∈ GrpOp
6 1 2 grpodivcl ⊢ G ∈ GrpOp ∧ A ∈ X ∧ C ∈ X → A D C ∈ X
7 5 6 syl3an1 ⊢ G ∈ AbelOp ∧ A ∈ X ∧ C ∈ X → A D C ∈ X
8 7 3adant3r2 ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D C ∈ X
9 3 4 8 3jca ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A ∈ X ∧ B ∈ X ∧ A D C ∈ X
10 1 2 ablodiv32 ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ A D C ∈ X → A D B D A D C = A D A D C D B
11 9 10 syldan ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D B D A D C = A D A D C D B
12 1 2 ablonncan ⊢ G ∈ AbelOp ∧ A ∈ X ∧ C ∈ X → A D A D C = C
13 12 3adant3r2 ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D A D C = C
14 13 oveq1d ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D A D C D B = C D B
15 11 14 eqtrd ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X ∧ C ∈ X → A D B D A D C = C D B