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