# Metamath Proof Explorer

## Theorem ablo32

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 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}$

### Proof

Step Hyp Ref Expression
1 ablcom.1 ${⊢}{X}=\mathrm{ran}{G}$
2 1 ablocom ${⊢}\left({G}\in \mathrm{AbelOp}\wedge {B}\in {X}\wedge {C}\in {X}\right)\to {B}{G}{C}={C}{G}{B}$
3 2 3adant3r1 ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to {B}{G}{C}={C}{G}{B}$
4 3 oveq2d ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to {A}{G}\left({B}{G}{C}\right)={A}{G}\left({C}{G}{B}\right)$
5 ablogrpo ${⊢}{G}\in \mathrm{AbelOp}\to {G}\in \mathrm{GrpOp}$
6 1 grpoass ${⊢}\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}{C}={A}{G}\left({B}{G}{C}\right)$
7 5 6 sylan ${⊢}\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}={A}{G}\left({B}{G}{C}\right)$
8 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)$
9 1 grpoass ${⊢}\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){G}{B}={A}{G}\left({C}{G}{B}\right)$
10 8 9 sylan2b ${⊢}\left({G}\in \mathrm{GrpOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{G}{C}\right){G}{B}={A}{G}\left({C}{G}{B}\right)$
11 5 10 sylan ${⊢}\left({G}\in \mathrm{AbelOp}\wedge \left({A}\in {X}\wedge {B}\in {X}\wedge {C}\in {X}\right)\right)\to \left({A}{G}{C}\right){G}{B}={A}{G}\left({C}{G}{B}\right)$
12 4 7 11 3eqtr4d ${⊢}\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}$