This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem ablocom

Description: An Abelian group operation is commutative. (Contributed by NM, 2-Nov-2006) (New usage is discouraged.)

Ref Expression
Hypothesis ablcom.1 
|- X = ran G
Assertion ablocom 
|- ( ( G e. AbelOp /\ A e. X /\ B e. X ) -> ( A G B ) = ( B G A ) )

Proof

Step Hyp Ref Expression
1 ablcom.1 
 |-  X = ran G
2 1 isablo 
 |-  ( G e. AbelOp <-> ( G e. GrpOp /\ A. x e. X A. y e. X ( x G y ) = ( y G x ) ) )
3 2 simprbi 
 |-  ( G e. AbelOp -> A. x e. X A. y e. X ( x G y ) = ( y G x ) )
4 oveq1 
 |-  ( x = A -> ( x G y ) = ( A G y ) )
5 oveq2 
 |-  ( x = A -> ( y G x ) = ( y G A ) )
6 4 5 eqeq12d 
 |-  ( x = A -> ( ( x G y ) = ( y G x ) <-> ( A G y ) = ( y G A ) ) )
7 oveq2 
 |-  ( y = B -> ( A G y ) = ( A G B ) )
8 oveq1 
 |-  ( y = B -> ( y G A ) = ( B G A ) )
9 7 8 eqeq12d 
 |-  ( y = B -> ( ( A G y ) = ( y G A ) <-> ( A G B ) = ( B G A ) ) )
10 6 9 rspc2v 
 |-  ( ( A e. X /\ B e. X ) -> ( A. x e. X A. y e. X ( x G y ) = ( y G x ) -> ( A G B ) = ( B G A ) ) )
11 3 10 syl5com 
 |-  ( G e. AbelOp -> ( ( A e. X /\ B e. X ) -> ( A G B ) = ( B G A ) ) )
12 11 3impib 
 |-  ( ( G e. AbelOp /\ A e. X /\ B e. X ) -> ( A G B ) = ( B G A ) )