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 = ran G
Assertion ablo32 
|- ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G B ) G C ) = ( ( A G C ) G B ) )

Proof

Step Hyp Ref Expression
1 ablcom.1 
 |-  X = ran G
2 1 ablocom 
 |-  ( ( G e. AbelOp /\ B e. X /\ C e. X ) -> ( B G C ) = ( C G B ) )
3 2 3adant3r1 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( B G C ) = ( C G B ) )
4 3 oveq2d 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( A G ( B G C ) ) = ( A G ( C G B ) ) )
5 ablogrpo 
 |-  ( G e. AbelOp -> G e. GrpOp )
6 1 grpoass 
 |-  ( ( G e. GrpOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G B ) G C ) = ( A G ( B G C ) ) )
7 5 6 sylan 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G B ) G C ) = ( A G ( B G C ) ) )
8 3ancomb 
 |-  ( ( A e. X /\ B e. X /\ C e. X ) <-> ( A e. X /\ C e. X /\ B e. X ) )
9 1 grpoass 
 |-  ( ( G e. GrpOp /\ ( A e. X /\ C e. X /\ B e. X ) ) -> ( ( A G C ) G B ) = ( A G ( C G B ) ) )
10 8 9 sylan2b 
 |-  ( ( G e. GrpOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G C ) G B ) = ( A G ( C G B ) ) )
11 5 10 sylan 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G C ) G B ) = ( A G ( C G B ) ) )
12 4 7 11 3eqtr4d 
 |-  ( ( G e. AbelOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G B ) G C ) = ( ( A G C ) G B ) )