Metamath Proof Explorer

Theorem gagrp

Description: The left argument of a group action is a group. (Contributed by Jeff Hankins, 11-Aug-2009) (Revised by Mario Carneiro, 30-Apr-2015)

Ref Expression
Assertion gagrp 
|- ( .(+) e. ( G GrpAct Y ) -> G e. Grp )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` G ) = ( 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 ) /\ ( .(+) : ( ( Base ` G ) X. Y ) --> Y /\ A. x e. Y ( ( ( 0g ` G ) .(+) x ) = x /\ A. y e. ( Base ` G ) A. z e. ( Base ` G ) ( ( y ( +g ` G ) z ) .(+) x ) = ( y .(+) ( z .(+) x ) ) ) ) ) )
5 4 simplbi 
 |-  ( .(+) e. ( G GrpAct Y ) -> ( G e. Grp /\ Y e. _V ) )
6 5 simpld 
 |-  ( .(+) e. ( G GrpAct Y ) -> G e. Grp )