# Metamath Proof Explorer

## Theorem grpomuldivass

Description: Associative-type law for multiplication and division. (Contributed by NM, 15-Feb-2008) (New usage is discouraged.)

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

### Proof

Step Hyp Ref Expression
1 grpdivf.1 ${⊢}{X}=\mathrm{ran}{G}$
2 grpdivf.3 ${⊢}{D}={/}_{g}\left({G}\right)$
3 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}$
4 simpr2 ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to {B}\in {X}$
5 eqid ${⊢}\mathrm{inv}\left({G}\right)=\mathrm{inv}\left({G}\right)$
6 1 5 grpoinvcl ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {C}\in {X}\right)\to \mathrm{inv}\left({G}\right)\left({C}\right)\in {X}$
7 6 3ad2antr3 ${⊢}\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({C}\right)\in {X}$
8 3 4 7 3jca ${⊢}\left({G}\in \mathrm{GrpOp}\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 \mathrm{inv}\left({G}\right)\left({C}\right)\in {X}\right)$
9 1 grpoass ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge \mathrm{inv}\left({G}\right)\left({C}\right)\in {X}\right)\right)\to \left({A}{G}{B}\right){G}\mathrm{inv}\left({G}\right)\left({C}\right)={A}{G}\left({B}{G}\mathrm{inv}\left({G}\right)\left({C}\right)\right)$
10 8 9 syldan ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{G}{B}\right){G}\mathrm{inv}\left({G}\right)\left({C}\right)={A}{G}\left({B}{G}\mathrm{inv}\left({G}\right)\left({C}\right)\right)$
11 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}$
12 1 grpocl ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{G}{B}\in {X}$
13 12 3adant3r3 ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to {A}{G}{B}\in {X}$
14 simpr3 ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to {C}\in {X}$
15 1 5 2 grpodivval ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {A}{G}{B}\in {X}\wedge {C}\in {X}\right)\to \left({A}{G}{B}\right){D}{C}=\left({A}{G}{B}\right){G}\mathrm{inv}\left({G}\right)\left({C}\right)$
16 11 13 14 15 syl3anc ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{G}{B}\right){D}{C}=\left({A}{G}{B}\right){G}\mathrm{inv}\left({G}\right)\left({C}\right)$
17 1 5 2 grpodivval ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {B}\in {X}\wedge {C}\in {X}\right)\to {B}{D}{C}={B}{G}\mathrm{inv}\left({G}\right)\left({C}\right)$
18 17 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}={B}{G}\mathrm{inv}\left({G}\right)\left({C}\right)$
19 18 oveq2d ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to {A}{G}\left({B}{D}{C}\right)={A}{G}\left({B}{G}\mathrm{inv}\left({G}\right)\left({C}\right)\right)$
20 10 16 19 3eqtr4d ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{G}{B}\right){D}{C}={A}{G}\left({B}{D}{C}\right)$