# Metamath Proof Explorer

## Theorem ablo4

Description: Commutative/associative law for Abelian groups. (Contributed by NM, 26-Apr-2007) (New usage is discouraged.)

Ref Expression
Hypothesis ablcom.1 ${⊢}{X}=\mathrm{ran}{G}$
Assertion ablo4 ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\right)\wedge \left({C}\in {X}\wedge {D}\in {X}\right)\right)\to \left({A}{G}{B}\right){G}\left({C}{G}{D}\right)=\left({A}{G}{C}\right){G}\left({B}{G}{D}\right)$

### Proof

Step Hyp Ref Expression
1 ablcom.1 ${⊢}{X}=\mathrm{ran}{G}$
2 simprll ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left(\left({A}\in {X}\wedge {B}\in {X}\right)\wedge \left({C}\in {X}\wedge {D}\in {X}\right)\right)\right)\to {A}\in {X}$
3 simprlr ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left(\left({A}\in {X}\wedge {B}\in {X}\right)\wedge \left({C}\in {X}\wedge {D}\in {X}\right)\right)\right)\to {B}\in {X}$
4 simprrl ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left(\left({A}\in {X}\wedge {B}\in {X}\right)\wedge \left({C}\in {X}\wedge {D}\in {X}\right)\right)\right)\to {C}\in {X}$
5 2 3 4 3jca ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left(\left({A}\in {X}\wedge {B}\in {X}\right)\wedge \left({C}\in {X}\wedge {D}\in {X}\right)\right)\right)\to \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)$
6 1 ablo32 ${⊢}\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){G}{C}=\left({A}{G}{C}\right){G}{B}$
7 5 6 syldan ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left(\left({A}\in {X}\wedge {B}\in {X}\right)\wedge \left({C}\in {X}\wedge {D}\in {X}\right)\right)\right)\to \left({A}{G}{B}\right){G}{C}=\left({A}{G}{C}\right){G}{B}$
8 7 oveq1d ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left(\left({A}\in {X}\wedge {B}\in {X}\right)\wedge \left({C}\in {X}\wedge {D}\in {X}\right)\right)\right)\to \left(\left({A}{G}{B}\right){G}{C}\right){G}{D}=\left(\left({A}{G}{C}\right){G}{B}\right){G}{D}$
9 ablogrpo ${⊢}{G}\in \mathrm{AbelOp}\to {G}\in \mathrm{GrpOp}$
10 1 grpocl ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\wedge {B}\in {X}\right)\to {A}{G}{B}\in {X}$
11 10 3expb ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\right)\right)\to {A}{G}{B}\in {X}$
12 11 adantrr ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left(\left({A}\in {X}\wedge {B}\in {X}\right)\wedge \left({C}\in {X}\wedge {D}\in {X}\right)\right)\right)\to {A}{G}{B}\in {X}$
13 simprrl ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left(\left({A}\in {X}\wedge {B}\in {X}\right)\wedge \left({C}\in {X}\wedge {D}\in {X}\right)\right)\right)\to {C}\in {X}$
14 simprrr ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left(\left({A}\in {X}\wedge {B}\in {X}\right)\wedge \left({C}\in {X}\wedge {D}\in {X}\right)\right)\right)\to {D}\in {X}$
15 12 13 14 3jca ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left(\left({A}\in {X}\wedge {B}\in {X}\right)\wedge \left({C}\in {X}\wedge {D}\in {X}\right)\right)\right)\to \left({A}{G}{B}\in {X}\wedge {C}\in {X}\wedge {D}\in {X}\right)$
16 1 grpoass ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({A}{G}{B}\in {X}\wedge {C}\in {X}\wedge {D}\in {X}\right)\right)\to \left(\left({A}{G}{B}\right){G}{C}\right){G}{D}=\left({A}{G}{B}\right){G}\left({C}{G}{D}\right)$
17 15 16 syldan ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left(\left({A}\in {X}\wedge {B}\in {X}\right)\wedge \left({C}\in {X}\wedge {D}\in {X}\right)\right)\right)\to \left(\left({A}{G}{B}\right){G}{C}\right){G}{D}=\left({A}{G}{B}\right){G}\left({C}{G}{D}\right)$
18 9 17 sylan ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left(\left({A}\in {X}\wedge {B}\in {X}\right)\wedge \left({C}\in {X}\wedge {D}\in {X}\right)\right)\right)\to \left(\left({A}{G}{B}\right){G}{C}\right){G}{D}=\left({A}{G}{B}\right){G}\left({C}{G}{D}\right)$
19 1 grpocl ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {A}\in {X}\wedge {C}\in {X}\right)\to {A}{G}{C}\in {X}$
20 19 3expb ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({A}\in {X}\wedge {C}\in {X}\right)\right)\to {A}{G}{C}\in {X}$
21 20 adantrlr ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left(\left({A}\in {X}\wedge {B}\in {X}\right)\wedge {C}\in {X}\right)\right)\to {A}{G}{C}\in {X}$
22 21 adantrrr ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left(\left({A}\in {X}\wedge {B}\in {X}\right)\wedge \left({C}\in {X}\wedge {D}\in {X}\right)\right)\right)\to {A}{G}{C}\in {X}$
23 simprlr ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left(\left({A}\in {X}\wedge {B}\in {X}\right)\wedge \left({C}\in {X}\wedge {D}\in {X}\right)\right)\right)\to {B}\in {X}$
24 22 23 14 3jca ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left(\left({A}\in {X}\wedge {B}\in {X}\right)\wedge \left({C}\in {X}\wedge {D}\in {X}\right)\right)\right)\to \left({A}{G}{C}\in {X}\wedge {B}\in {X}\wedge {D}\in {X}\right)$
25 1 grpoass ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({A}{G}{C}\in {X}\wedge {B}\in {X}\wedge {D}\in {X}\right)\right)\to \left(\left({A}{G}{C}\right){G}{B}\right){G}{D}=\left({A}{G}{C}\right){G}\left({B}{G}{D}\right)$
26 24 25 syldan ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left(\left({A}\in {X}\wedge {B}\in {X}\right)\wedge \left({C}\in {X}\wedge {D}\in {X}\right)\right)\right)\to \left(\left({A}{G}{C}\right){G}{B}\right){G}{D}=\left({A}{G}{C}\right){G}\left({B}{G}{D}\right)$
27 9 26 sylan ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left(\left({A}\in {X}\wedge {B}\in {X}\right)\wedge \left({C}\in {X}\wedge {D}\in {X}\right)\right)\right)\to \left(\left({A}{G}{C}\right){G}{B}\right){G}{D}=\left({A}{G}{C}\right){G}\left({B}{G}{D}\right)$
28 8 18 27 3eqtr3d ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left(\left({A}\in {X}\wedge {B}\in {X}\right)\wedge \left({C}\in {X}\wedge {D}\in {X}\right)\right)\right)\to \left({A}{G}{B}\right){G}\left({C}{G}{D}\right)=\left({A}{G}{C}\right){G}\left({B}{G}{D}\right)$
29 28 3impb ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\right)\wedge \left({C}\in {X}\wedge {D}\in {X}\right)\right)\to \left({A}{G}{B}\right){G}\left({C}{G}{D}\right)=\left({A}{G}{C}\right){G}\left({B}{G}{D}\right)$