Metamath Proof Explorer

Theorem grpoass

Description: A group operation is associative. (Contributed by NM, 10-Oct-2006) (New usage is discouraged.)

Ref Expression
Hypothesis grpfo.1 
|- X = ran G
Assertion grpoass 
|- ( ( G e. GrpOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G B ) G C ) = ( A G ( B G C ) ) )

Proof

Step Hyp Ref Expression
1 grpfo.1 
 |-  X = ran G
2 1 isgrpo 
 |-  ( G e. GrpOp -> ( G e. GrpOp <-> ( G : ( X X. X ) --> X /\ A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. u e. X A. x e. X ( ( u G x ) = x /\ E. y e. X ( y G x ) = u ) ) ) )
3 2 ibi 
 |-  ( G e. GrpOp -> ( G : ( X X. X ) --> X /\ A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) /\ E. u e. X A. x e. X ( ( u G x ) = x /\ E. y e. X ( y G x ) = u ) ) )
4 3 simp2d 
 |-  ( G e. GrpOp -> A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) )
5 oveq1 
 |-  ( x = A -> ( x G y ) = ( A G y ) )
6 5 oveq1d 
 |-  ( x = A -> ( ( x G y ) G z ) = ( ( A G y ) G z ) )
7 oveq1 
 |-  ( x = A -> ( x G ( y G z ) ) = ( A G ( y G z ) ) )
8 6 7 eqeq12d 
 |-  ( x = A -> ( ( ( x G y ) G z ) = ( x G ( y G z ) ) <-> ( ( A G y ) G z ) = ( A G ( y G z ) ) ) )
9 oveq2 
 |-  ( y = B -> ( A G y ) = ( A G B ) )
10 9 oveq1d 
 |-  ( y = B -> ( ( A G y ) G z ) = ( ( A G B ) G z ) )
11 oveq1 
 |-  ( y = B -> ( y G z ) = ( B G z ) )
12 11 oveq2d 
 |-  ( y = B -> ( A G ( y G z ) ) = ( A G ( B G z ) ) )
13 10 12 eqeq12d 
 |-  ( y = B -> ( ( ( A G y ) G z ) = ( A G ( y G z ) ) <-> ( ( A G B ) G z ) = ( A G ( B G z ) ) ) )
14 oveq2 
 |-  ( z = C -> ( ( A G B ) G z ) = ( ( A G B ) G C ) )
15 oveq2 
 |-  ( z = C -> ( B G z ) = ( B G C ) )
16 15 oveq2d 
 |-  ( z = C -> ( A G ( B G z ) ) = ( A G ( B G C ) ) )
17 14 16 eqeq12d 
 |-  ( z = C -> ( ( ( A G B ) G z ) = ( A G ( B G z ) ) <-> ( ( A G B ) G C ) = ( A G ( B G C ) ) ) )
18 8 13 17 rspc3v 
 |-  ( ( A e. X /\ B e. X /\ C e. X ) -> ( A. x e. X A. y e. X A. z e. X ( ( x G y ) G z ) = ( x G ( y G z ) ) -> ( ( A G B ) G C ) = ( A G ( B G C ) ) ) )
19 4 18 mpan9 
 |-  ( ( G e. GrpOp /\ ( A e. X /\ B e. X /\ C e. X ) ) -> ( ( A G B ) G C ) = ( A G ( B G C ) ) )