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→ADADB=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→ADADB=ADAGB
6 4 5 sylan2 ⊢G∈AbelOp∧A∈X∧B∈X→ADADB=ADAGB
7 6 3impb ⊢G∈AbelOp∧A∈X∧B∈X→ADADB=ADAGB
8 ablogrpo ⊢G∈AbelOp→G∈GrpOp
9 eqid ⊢GId⁡G=GId⁡G
10 1 2 9 grpodivid ⊢G∈GrpOp∧A∈X→ADA=GId⁡G
11 8 10 sylan ⊢G∈AbelOp∧A∈X→ADA=GId⁡G
12 11 3adant3 ⊢G∈AbelOp∧A∈X∧B∈X→ADA=GId⁡G
13 12 oveq1d ⊢G∈AbelOp∧A∈X∧B∈X→ADAGB=GId⁡GGB
14 1 9 grpolid ⊢G∈GrpOp∧B∈X→GId⁡GGB=B
15 8 14 sylan ⊢G∈AbelOp∧B∈X→GId⁡GGB=B
16 15 3adant2 ⊢G∈AbelOp∧A∈X∧B∈X→GId⁡GGB=B
17 7 13 16 3eqtrd ⊢G∈AbelOp∧A∈X∧B∈X→ADADB=B