Theorem cayleylem2

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	cayleylem2	|- ( G e. Grp -> F : X -1-1-> S )

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		fveq1	|- ( ( F ` x ) = ( 0g ` H ) -> ( ( F ` x ) ` .0. ) = ( ( 0g ` H ) ` .0. ) )
8		simpr	|- ( ( G e. Grp /\ x e. X ) -> x e. X )
9	1 3	grpidcl	|- ( G e. Grp -> .0. e. X )
10	9	adantr	|- ( ( G e. Grp /\ x e. X ) -> .0. e. X )
11	6 1	grplactval	|- ( ( x e. X /\ .0. e. X ) -> ( ( F ` x ) ` .0. ) = ( x .+ .0. ) )
12	8 10 11	syl2anc	|- ( ( G e. Grp /\ x e. X ) -> ( ( F ` x ) ` .0. ) = ( x .+ .0. ) )
13	1 2 3	grprid	|- ( ( G e. Grp /\ x e. X ) -> ( x .+ .0. ) = x )
14	12 13	eqtrd	|- ( ( G e. Grp /\ x e. X ) -> ( ( F ` x ) ` .0. ) = x )
15	1	fvexi	|- X e. _V
16	4	symgid	|- ( X e. _V -> ( _I |` X ) = ( 0g ` H ) )
17	15 16	ax-mp	|- ( _I |` X ) = ( 0g ` H )
18	17	fveq1i	|- ( ( _I |` X ) ` .0. ) = ( ( 0g ` H ) ` .0. )
19		fvresi	|- ( .0. e. X -> ( ( _I |` X ) ` .0. ) = .0. )
20	10 19	syl	|- ( ( G e. Grp /\ x e. X ) -> ( ( _I |` X ) ` .0. ) = .0. )
21	18 20	eqtr3id	|- ( ( G e. Grp /\ x e. X ) -> ( ( 0g ` H ) ` .0. ) = .0. )
22	14 21	eqeq12d	|- ( ( G e. Grp /\ x e. X ) -> ( ( ( F ` x ) ` .0. ) = ( ( 0g ` H ) ` .0. ) <-> x = .0. ) )
23	7 22	syl5ib	|- ( ( G e. Grp /\ x e. X ) -> ( ( F ` x ) = ( 0g ` H ) -> x = .0. ) )
24	23	ralrimiva	|- ( G e. Grp -> A. x e. X ( ( F ` x ) = ( 0g ` H ) -> x = .0. ) )
25	1 2 3 4 5 6	cayleylem1	|- ( G e. Grp -> F e. ( G GrpHom H ) )
26		eqid	|- ( 0g ` H ) = ( 0g ` H )
27	1 5 3 26	ghmf1	|- ( F e. ( G GrpHom H ) -> ( F : X -1-1-> S <-> A. x e. X ( ( F ` x ) = ( 0g ` H ) -> x = .0. ) ) )
28	25 27	syl	|- ( G e. Grp -> ( F : X -1-1-> S <-> A. x e. X ( ( F ` x ) = ( 0g ` H ) -> x = .0. ) ) )
29	24 28	mpbird	|- ( G e. Grp -> F : X -1-1-> S )