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

### Proof

Step Hyp Ref Expression
1 abldiv.1 ${⊢}{X}=\mathrm{ran}{G}$
2 abldiv.3 ${⊢}{D}={/}_{g}\left({G}\right)$
3 id ${⊢}\left({A}\in {X}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to \left({A}\in {X}\wedge {A}\in {X}\wedge {B}\in {X}\right)$
4 3 3anidm12 ${⊢}\left({A}\in {X}\wedge {B}\in {X}\right)\to \left({A}\in {X}\wedge {A}\in {X}\wedge {B}\in {X}\right)$
5 1 2 ablodivdiv ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {A}\in {X}\wedge {B}\in {X}\right)\right)\to {A}{D}\left({A}{D}{B}\right)=\left({A}{D}{A}\right){G}{B}$
6 4 5 sylan2 ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\right)\right)\to {A}{D}\left({A}{D}{B}\right)=\left({A}{D}{A}\right){G}{B}$
7 6 3impb ${⊢}\left({G}\in \mathrm{AbelOp}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{D}\left({A}{D}{B}\right)=\left({A}{D}{A}\right){G}{B}$
8 ablogrpo ${⊢}{G}\in \mathrm{AbelOp}\to {G}\in \mathrm{GrpOp}$
9 eqid ${⊢}\mathrm{GId}\left({G}\right)=\mathrm{GId}\left({G}\right)$
10 1 2 9 grpodivid ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\right)\to {A}{D}{A}=\mathrm{GId}\left({G}\right)$
11 8 10 sylan ${⊢}\left({G}\in \mathrm{AbelOp}\wedge {A}\in {X}\right)\to {A}{D}{A}=\mathrm{GId}\left({G}\right)$
12 11 3adant3 ${⊢}\left({G}\in \mathrm{AbelOp}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{D}{A}=\mathrm{GId}\left({G}\right)$
13 12 oveq1d ${⊢}\left({G}\in \mathrm{AbelOp}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to \left({A}{D}{A}\right){G}{B}=\mathrm{GId}\left({G}\right){G}{B}$
14 1 9 grpolid ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {B}\in {X}\right)\to \mathrm{GId}\left({G}\right){G}{B}={B}$
15 8 14 sylan ${⊢}\left({G}\in \mathrm{AbelOp}\wedge {B}\in {X}\right)\to \mathrm{GId}\left({G}\right){G}{B}={B}$
16 15 3adant2 ${⊢}\left({G}\in \mathrm{AbelOp}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to \mathrm{GId}\left({G}\right){G}{B}={B}$
17 7 13 16 3eqtrd ${⊢}\left({G}\in \mathrm{AbelOp}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{D}\left({A}{D}{B}\right)={B}$