Theorem cayleylem1

Description: Lemma for cayley . (Contributed by Paul Chapman, 3-Mar-2008) (Revised by Mario Carneiro, 13-Jan-2015)

	Ref	Expression
Hypotheses	cayleylem1.x	|- X = ( Base ` G )
	cayleylem1.p	|- .+ = ( +g ` G )
	cayleylem1.u	|- .0. = ( 0g ` G )
	cayleylem1.h	|- H = ( SymGrp ` X )
	cayleylem1.s	|- S = ( Base ` H )
	cayleylem1.f	|- F = ( g e. X |-> ( a e. X |-> ( g .+ a ) ) )
Assertion	cayleylem1	|- ( G e. Grp -> F e. ( G GrpHom H ) )

Proof

Step	Hyp	Ref	Expression
1		cayleylem1.x	|- X = ( Base ` G )
2		cayleylem1.p	|- .+ = ( +g ` G )
3		cayleylem1.u	|- .0. = ( 0g ` G )
4		cayleylem1.h	|- H = ( SymGrp ` X )
5		cayleylem1.s	|- S = ( Base ` H )
6		cayleylem1.f	|- F = ( g e. X |-> ( a e. X |-> ( g .+ a ) ) )
7		eqid	|- ( x e. X , y e. X |-> ( x .+ y ) ) = ( x e. X , y e. X |-> ( x .+ y ) )
8	1 2 7	gaid2	|- ( G e. Grp -> ( x e. X , y e. X |-> ( x .+ y ) ) e. ( G GrpAct X ) )
9		oveq12	|- ( ( x = g /\ y = a ) -> ( x .+ y ) = ( g .+ a ) )
10		ovex	|- ( g .+ a ) e. _V
11	9 7 10	ovmpoa	|- ( ( g e. X /\ a e. X ) -> ( g ( x e. X , y e. X |-> ( x .+ y ) ) a ) = ( g .+ a ) )
12	11	mpteq2dva	|- ( g e. X -> ( a e. X |-> ( g ( x e. X , y e. X |-> ( x .+ y ) ) a ) ) = ( a e. X |-> ( g .+ a ) ) )
13	12	mpteq2ia	|- ( g e. X |-> ( a e. X |-> ( g ( x e. X , y e. X |-> ( x .+ y ) ) a ) ) ) = ( g e. X |-> ( a e. X |-> ( g .+ a ) ) )
14	6 13	eqtr4i	|- F = ( g e. X |-> ( a e. X |-> ( g ( x e. X , y e. X |-> ( x .+ y ) ) a ) ) )
15	1 4 14	galactghm	|- ( ( x e. X , y e. X |-> ( x .+ y ) ) e. ( G GrpAct X ) -> F e. ( G GrpHom H ) )
16	8 15	syl	|- ( G e. Grp -> F e. ( G GrpHom H ) )