# Metamath Proof Explorer

## Theorem ablodivdiv

Description: Law for double group division. (Contributed by NM, 29-Feb-2008) (New usage is discouraged.)

Ref Expression
Hypotheses abldiv.1 ${⊢}{X}=\mathrm{ran}{G}$
abldiv.3 ${⊢}{D}={/}_{g}\left({G}\right)$
Assertion ablodivdiv ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to {A}{D}\left({B}{D}{C}\right)=\left({A}{D}{B}\right){G}{C}$

### Proof

Step Hyp Ref Expression
1 abldiv.1 ${⊢}{X}=\mathrm{ran}{G}$
2 abldiv.3 ${⊢}{D}={/}_{g}\left({G}\right)$
3 ablogrpo ${⊢}{G}\in \mathrm{AbelOp}\to {G}\in \mathrm{GrpOp}$
4 1 2 grpodivdiv ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to {A}{D}\left({B}{D}{C}\right)={A}{G}\left({C}{D}{B}\right)$
5 3 4 sylan ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to {A}{D}\left({B}{D}{C}\right)={A}{G}\left({C}{D}{B}\right)$
6 3ancomb ${⊢}\left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)↔\left({A}\in {X}\wedge {C}\in {X}\wedge {B}\in {X}\right)$
7 1 2 grpomuldivass ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({A}\in {X}\wedge {C}\in {X}\wedge {B}\in {X}\right)\right)\to \left({A}{G}{C}\right){D}{B}={A}{G}\left({C}{D}{B}\right)$
8 3 7 sylan ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {C}\in {X}\wedge {B}\in {X}\right)\right)\to \left({A}{G}{C}\right){D}{B}={A}{G}\left({C}{D}{B}\right)$
9 1 2 ablomuldiv ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {C}\in {X}\wedge {B}\in {X}\right)\right)\to \left({A}{G}{C}\right){D}{B}=\left({A}{D}{B}\right){G}{C}$
10 8 9 eqtr3d ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {C}\in {X}\wedge {B}\in {X}\right)\right)\to {A}{G}\left({C}{D}{B}\right)=\left({A}{D}{B}\right){G}{C}$
11 6 10 sylan2b ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to {A}{G}\left({C}{D}{B}\right)=\left({A}{D}{B}\right){G}{C}$
12 5 11 eqtrd ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to {A}{D}\left({B}{D}{C}\right)=\left({A}{D}{B}\right){G}{C}$