Metamath Proof Explorer

Theorem ablonncan

Description: Cancellation law for group division. ( nncan 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 ablonncan ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X → A D A D B = B

Proof

Step Hyp Ref Expression
1 abldiv.1 ⊢ X = ran ⁡ G
2 abldiv.3 ⊢ D = / g ⁡ G
3 id ⊢ A ∈ X ∧ A ∈ X ∧ B ∈ X → A ∈ X ∧ A ∈ X ∧ B ∈ X
4 3 3anidm12 ⊢ A ∈ X ∧ B ∈ X → A ∈ X ∧ A ∈ X ∧ B ∈ X
5 1 2 ablodivdiv ⊢ G ∈ AbelOp ∧ A ∈ X ∧ A ∈ X ∧ B ∈ X → A D A D B = A D A G B
6 4 5 sylan2 ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X → A D A D B = A D A G B
7 6 3impb ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X → A D A D B = A D A G B
8 ablogrpo ⊢ G ∈ AbelOp → G ∈ GrpOp
9 eqid ⊢ GId ⁡ G = GId ⁡ G
10 1 2 9 grpodivid ⊢ G ∈ GrpOp ∧ A ∈ X → A D A = GId ⁡ G
11 8 10 sylan ⊢ G ∈ AbelOp ∧ A ∈ X → A D A = GId ⁡ G
12 11 3adant3 ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X → A D A = GId ⁡ G
13 12 oveq1d ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X → A D A G B = GId ⁡ G G B
14 1 9 grpolid ⊢ G ∈ GrpOp ∧ B ∈ X → GId ⁡ G G B = B
15 8 14 sylan ⊢ G ∈ AbelOp ∧ B ∈ X → GId ⁡ G G B = B
16 15 3adant2 ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X → GId ⁡ G G B = B
17 7 13 16 3eqtrd ⊢ G ∈ AbelOp ∧ A ∈ X ∧ B ∈ X → A D A D B = B