Metamath Proof Explorer

Theorem gaass

Description: An "associative" property for group actions. (Contributed by Jeff Hankins, 11-Aug-2009) (Revised by Mario Carneiro, 13-Jan-2015)

Ref Expression
Hypotheses gaass.1 
|- X = ( Base ` G )
gaass.2 
|- .+ = ( +g ` G )
Assertion gaass 
|- ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. X /\ C e. Y ) ) -> ( ( A .+ B ) .(+) C ) = ( A .(+) ( B .(+) C ) ) )

Proof

Step Hyp Ref Expression
1 gaass.1 
 |-  X = ( Base ` G )
2 gaass.2 
 |-  .+ = ( +g ` G )
3 eqid 
 |-  ( 0g ` G ) = ( 0g ` G )
4 1 2 3 isga 
 |-  ( .(+) e. ( G GrpAct Y ) <-> ( ( G e. Grp /\ Y e. _V ) /\ ( .(+) : ( X X. Y ) --> Y /\ A. x e. Y ( ( ( 0g ` G ) .(+) x ) = x /\ A. y e. X A. z e. X ( ( y .+ z ) .(+) x ) = ( y .(+) ( z .(+) x ) ) ) ) ) )
5 4 simprbi 
 |-  ( .(+) e. ( G GrpAct Y ) -> ( .(+) : ( X X. Y ) --> Y /\ A. x e. Y ( ( ( 0g ` G ) .(+) x ) = x /\ A. y e. X A. z e. X ( ( y .+ z ) .(+) x ) = ( y .(+) ( z .(+) x ) ) ) ) )
6 simpr 
 |-  ( ( ( ( 0g ` G ) .(+) x ) = x /\ A. y e. X A. z e. X ( ( y .+ z ) .(+) x ) = ( y .(+) ( z .(+) x ) ) ) -> A. y e. X A. z e. X ( ( y .+ z ) .(+) x ) = ( y .(+) ( z .(+) x ) ) )
7 6 ralimi 
 |-  ( A. x e. Y ( ( ( 0g ` G ) .(+) x ) = x /\ A. y e. X A. z e. X ( ( y .+ z ) .(+) x ) = ( y .(+) ( z .(+) x ) ) ) -> A. x e. Y A. y e. X A. z e. X ( ( y .+ z ) .(+) x ) = ( y .(+) ( z .(+) x ) ) )
8 5 7 simpl2im 
 |-  ( .(+) e. ( G GrpAct Y ) -> A. x e. Y A. y e. X A. z e. X ( ( y .+ z ) .(+) x ) = ( y .(+) ( z .(+) x ) ) )
9 oveq2 
 |-  ( x = C -> ( ( y .+ z ) .(+) x ) = ( ( y .+ z ) .(+) C ) )
10 oveq2 
 |-  ( x = C -> ( z .(+) x ) = ( z .(+) C ) )
11 10 oveq2d 
 |-  ( x = C -> ( y .(+) ( z .(+) x ) ) = ( y .(+) ( z .(+) C ) ) )
12 9 11 eqeq12d 
 |-  ( x = C -> ( ( ( y .+ z ) .(+) x ) = ( y .(+) ( z .(+) x ) ) <-> ( ( y .+ z ) .(+) C ) = ( y .(+) ( z .(+) C ) ) ) )
13 oveq1 
 |-  ( y = A -> ( y .+ z ) = ( A .+ z ) )
14 13 oveq1d 
 |-  ( y = A -> ( ( y .+ z ) .(+) C ) = ( ( A .+ z ) .(+) C ) )
15 oveq1 
 |-  ( y = A -> ( y .(+) ( z .(+) C ) ) = ( A .(+) ( z .(+) C ) ) )
16 14 15 eqeq12d 
 |-  ( y = A -> ( ( ( y .+ z ) .(+) C ) = ( y .(+) ( z .(+) C ) ) <-> ( ( A .+ z ) .(+) C ) = ( A .(+) ( z .(+) C ) ) ) )
17 oveq2 
 |-  ( z = B -> ( A .+ z ) = ( A .+ B ) )
18 17 oveq1d 
 |-  ( z = B -> ( ( A .+ z ) .(+) C ) = ( ( A .+ B ) .(+) C ) )
19 oveq1 
 |-  ( z = B -> ( z .(+) C ) = ( B .(+) C ) )
20 19 oveq2d 
 |-  ( z = B -> ( A .(+) ( z .(+) C ) ) = ( A .(+) ( B .(+) C ) ) )
21 18 20 eqeq12d 
 |-  ( z = B -> ( ( ( A .+ z ) .(+) C ) = ( A .(+) ( z .(+) C ) ) <-> ( ( A .+ B ) .(+) C ) = ( A .(+) ( B .(+) C ) ) ) )
22 12 16 21 rspc3v 
 |-  ( ( C e. Y /\ A e. X /\ B e. X ) -> ( A. x e. Y A. y e. X A. z e. X ( ( y .+ z ) .(+) x ) = ( y .(+) ( z .(+) x ) ) -> ( ( A .+ B ) .(+) C ) = ( A .(+) ( B .(+) C ) ) ) )
23 8 22 syl5 
 |-  ( ( C e. Y /\ A e. X /\ B e. X ) -> ( .(+) e. ( G GrpAct Y ) -> ( ( A .+ B ) .(+) C ) = ( A .(+) ( B .(+) C ) ) ) )
24 23 3coml 
 |-  ( ( A e. X /\ B e. X /\ C e. Y ) -> ( .(+) e. ( G GrpAct Y ) -> ( ( A .+ B ) .(+) C ) = ( A .(+) ( B .(+) C ) ) ) )
25 24 impcom 
 |-  ( ( .(+) e. ( G GrpAct Y ) /\ ( A e. X /\ B e. X /\ C e. Y ) ) -> ( ( A .+ B ) .(+) C ) = ( A .(+) ( B .(+) C ) ) )