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 ) )