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→ADBDADC=CDB

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→ADC∈X
7 5 6 syl3an1 ⊢G∈AbelOp∧A∈X∧C∈X→ADC∈X
8 7 3adant3r2 ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X→ADC∈X
9 3 4 8 3jca ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X→A∈X∧B∈X∧ADC∈X
10 1 2 ablodiv32 ⊢G∈AbelOp∧A∈X∧B∈X∧ADC∈X→ADBDADC=ADADCDB
11 9 10 syldan ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X→ADBDADC=ADADCDB
12 1 2 ablonncan ⊢G∈AbelOp∧A∈X∧C∈X→ADADC=C
13 12 3adant3r2 ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X→ADADC=C
14 13 oveq1d ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X→ADADCDB=CDB
15 11 14 eqtrd ⊢G∈AbelOp∧A∈X∧B∈X∧C∈X→ADBDADC=CDB