Metamath Proof Explorer

Theorem gaf

Description: The mapping of the group action operation. (Contributed by Jeff Hankins, 11-Aug-2009) (Revised by Mario Carneiro, 13-Jan-2015)

Ref Expression
Hypothesis gaf.1 
|- X = ( Base ` G )
Assertion gaf 
|- ( .(+) e. ( G GrpAct Y ) -> .(+) : ( X X. Y ) --> Y )

Proof

Step Hyp Ref Expression
1 gaf.1 
 |-  X = ( Base ` G )
2 eqid 
 |-  ( +g ` G ) = ( +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 ( +g ` G ) 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 ( +g ` G ) z ) .(+) x ) = ( y .(+) ( z .(+) x ) ) ) ) )
6 5 simpld 
 |-  ( .(+) e. ( G GrpAct Y ) -> .(+) : ( X X. Y ) --> Y )