# Metamath Proof Explorer

## Theorem grpodivdiv

Description: Double group division. (Contributed by NM, 24-Feb-2008) (New usage is discouraged.)

Ref Expression
Hypotheses grpdivf.1 ${⊢}{X}=\mathrm{ran}{G}$
grpdivf.3 ${⊢}{D}={/}_{g}\left({G}\right)$
Assertion 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)$

### Proof

Step Hyp Ref Expression
1 grpdivf.1 ${⊢}{X}=\mathrm{ran}{G}$
2 grpdivf.3 ${⊢}{D}={/}_{g}\left({G}\right)$
3 simpl ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to {G}\in \mathrm{GrpOp}$
4 simpr1 ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to {A}\in {X}$
5 1 2 grpodivcl ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {B}\in {X}\wedge {C}\in {X}\right)\to {B}{D}{C}\in {X}$
6 5 3adant3r1 ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to {B}{D}{C}\in {X}$
7 eqid ${⊢}\mathrm{inv}\left({G}\right)=\mathrm{inv}\left({G}\right)$
8 1 7 2 grpodivval ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\wedge {B}{D}{C}\in {X}\right)\to {A}{D}\left({B}{D}{C}\right)={A}{G}\mathrm{inv}\left({G}\right)\left({B}{D}{C}\right)$
9 3 4 6 8 syl3anc ${⊢}\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}\mathrm{inv}\left({G}\right)\left({B}{D}{C}\right)$
10 1 7 2 grpoinvdiv ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {B}\in {X}\wedge {C}\in {X}\right)\to \mathrm{inv}\left({G}\right)\left({B}{D}{C}\right)={C}{D}{B}$
11 10 3adant3r1 ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \mathrm{inv}\left({G}\right)\left({B}{D}{C}\right)={C}{D}{B}$
12 11 oveq2d ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to {A}{G}\mathrm{inv}\left({G}\right)\left({B}{D}{C}\right)={A}{G}\left({C}{D}{B}\right)$
13 9 12 eqtrd ${⊢}\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)$