# 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}=\mathrm{ran}{G}$
abldiv.3 ${⊢}{D}={/}_{g}\left({G}\right)$
Assertion ablonnncan1 ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{D}{B}\right){D}\left({A}{D}{C}\right)={C}{D}{B}$

### Proof

Step Hyp Ref Expression
1 abldiv.1 ${⊢}{X}=\mathrm{ran}{G}$
2 abldiv.3 ${⊢}{D}={/}_{g}\left({G}\right)$
3 simpr1 ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to {A}\in {X}$
4 simpr2 ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to {B}\in {X}$
5 ablogrpo ${⊢}{G}\in \mathrm{AbelOp}\to {G}\in \mathrm{GrpOp}$
6 1 2 grpodivcl ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\wedge {C}\in {X}\right)\to {A}{D}{C}\in {X}$
7 5 6 syl3an1 ${⊢}\left({G}\in \mathrm{AbelOp}\wedge {A}\in {X}\wedge {C}\in {X}\right)\to {A}{D}{C}\in {X}$
8 7 3adant3r2 ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to {A}{D}{C}\in {X}$
9 3 4 8 3jca ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}\in {X}\wedge {B}\in {X}\wedge {A}{D}{C}\in {X}\right)$
10 1 2 ablodiv32 ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {A}{D}{C}\in {X}\right)\right)\to \left({A}{D}{B}\right){D}\left({A}{D}{C}\right)=\left({A}{D}\left({A}{D}{C}\right)\right){D}{B}$
11 9 10 syldan ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{D}{B}\right){D}\left({A}{D}{C}\right)=\left({A}{D}\left({A}{D}{C}\right)\right){D}{B}$
12 1 2 ablonncan ${⊢}\left({G}\in \mathrm{AbelOp}\wedge {A}\in {X}\wedge {C}\in {X}\right)\to {A}{D}\left({A}{D}{C}\right)={C}$
13 12 3adant3r2 ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to {A}{D}\left({A}{D}{C}\right)={C}$
14 13 oveq1d ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{D}\left({A}{D}{C}\right)\right){D}{B}={C}{D}{B}$
15 11 14 eqtrd ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{D}{B}\right){D}\left({A}{D}{C}\right)={C}{D}{B}$