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

Metamath Proof Explorer

Theorem gaid2

Description: A group operation is a left group action of the group on itself. (Contributed by FL, 17-May-2010) (Revised by Mario Carneiro, 13-Jan-2015)

Ref Expression
Hypotheses gaid2.1 
|- X = ( Base ` G )
gaid2.2 
|- .+ = ( +g ` G )
gaid2.3 
|- F = ( x e. X , y e. X |-> ( x .+ y ) )
Assertion gaid2 
|- ( G e. Grp -> F e. ( G GrpAct X ) )

Proof

Step Hyp Ref Expression
1 gaid2.1 
 |-  X = ( Base ` G )
2 gaid2.2 
 |-  .+ = ( +g ` G )
3 gaid2.3 
 |-  F = ( x e. X , y e. X |-> ( x .+ y ) )
4 1 subgid 
 |-  ( G e. Grp -> X e. ( SubGrp ` G ) )
5 eqid 
 |-  ( G |`s X ) = ( G |`s X )
6 1 2 5 3 subgga 
 |-  ( X e. ( SubGrp ` G ) -> F e. ( ( G |`s X ) GrpAct X ) )
7 4 6 syl 
 |-  ( G e. Grp -> F e. ( ( G |`s X ) GrpAct X ) )
8 1 ressid 
 |-  ( G e. Grp -> ( G |`s X ) = G )
9 8 oveq1d 
 |-  ( G e. Grp -> ( ( G |`s X ) GrpAct X ) = ( G GrpAct X ) )
10 7 9 eleqtrd 
 |-  ( G e. Grp -> F e. ( G GrpAct X ) )