# Metamath Proof Explorer

## Theorem ablomuldiv

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

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

### Proof

Step Hyp Ref Expression
1 abldiv.1 ${⊢}{X}=\mathrm{ran}{G}$
2 abldiv.3 ${⊢}{D}={/}_{g}\left({G}\right)$
3 1 ablocom ${⊢}\left({G}\in \mathrm{AbelOp}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{G}{B}={B}{G}{A}$
4 3 3adant3r3 ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to {A}{G}{B}={B}{G}{A}$
5 4 oveq1d ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{G}{B}\right){D}{C}=\left({B}{G}{A}\right){D}{C}$
6 3ancoma ${⊢}\left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)↔\left({B}\in {X}\wedge {A}\in {X}\wedge {C}\in {X}\right)$
7 ablogrpo ${⊢}{G}\in \mathrm{AbelOp}\to {G}\in \mathrm{GrpOp}$
8 1 2 grpomuldivass ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({B}\in {X}\wedge {A}\in {X}\wedge {C}\in {X}\right)\right)\to \left({B}{G}{A}\right){D}{C}={B}{G}\left({A}{D}{C}\right)$
9 7 8 sylan ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({B}\in {X}\wedge {A}\in {X}\wedge {C}\in {X}\right)\right)\to \left({B}{G}{A}\right){D}{C}={B}{G}\left({A}{D}{C}\right)$
10 6 9 sylan2b ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({B}{G}{A}\right){D}{C}={B}{G}\left({A}{D}{C}\right)$
11 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}$
12 1 2 grpodivcl ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\wedge {C}\in {X}\right)\to {A}{D}{C}\in {X}$
13 7 12 syl3an1 ${⊢}\left({G}\in \mathrm{AbelOp}\wedge {A}\in {X}\wedge {C}\in {X}\right)\to {A}{D}{C}\in {X}$
14 13 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}$
15 11 14 jca ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({B}\in {X}\wedge {A}{D}{C}\in {X}\right)$
16 1 ablocom ${⊢}\left({G}\in \mathrm{AbelOp}\wedge {B}\in {X}\wedge {A}{D}{C}\in {X}\right)\to {B}{G}\left({A}{D}{C}\right)=\left({A}{D}{C}\right){G}{B}$
17 16 3expb ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({B}\in {X}\wedge {A}{D}{C}\in {X}\right)\right)\to {B}{G}\left({A}{D}{C}\right)=\left({A}{D}{C}\right){G}{B}$
18 15 17 syldan ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to {B}{G}\left({A}{D}{C}\right)=\left({A}{D}{C}\right){G}{B}$
19 5 10 18 3eqtrd ${⊢}\left({G}\in \mathrm{AbelOp}\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}{D}{C}\right){G}{B}$