Theorem cayley

Description: Cayley's Theorem (constructive version): given group G , F is an isomorphism between G and the subgroup S of the symmetric group H on the underlying set X of G . See also Theorem 3.15 in Rotman p. 42. (Contributed by Paul Chapman, 3-Mar-2008) (Proof shortened by Mario Carneiro, 13-Jan-2015)

	Ref	Expression
Hypotheses	cayley.x	|- X = ( Base ` G )
	cayley.h	|- H = ( SymGrp ` X )
	cayley.p	|- .+ = ( +g ` G )
	cayley.f	|- F = ( g e. X |-> ( a e. X |-> ( g .+ a ) ) )
	cayley.s	|- S = ran F
Assertion	cayley	|- ( G e. Grp -> ( S e. ( SubGrp ` H ) /\ F e. ( G GrpHom ( H |`s S ) ) /\ F : X -1-1-onto-> S ) )

Proof

Step	Hyp	Ref	Expression
1		cayley.x	|- X = ( Base ` G )
2		cayley.h	|- H = ( SymGrp ` X )
3		cayley.p	|- .+ = ( +g ` G )
4		cayley.f	|- F = ( g e. X |-> ( a e. X |-> ( g .+ a ) ) )
5		cayley.s	|- S = ran F
6		eqid	|- ( 0g ` G ) = ( 0g ` G )
7		eqid	|- ( Base ` H ) = ( Base ` H )
8	1 3 6 2 7 4	cayleylem1	|- ( G e. Grp -> F e. ( G GrpHom H ) )
9		ghmrn	|- ( F e. ( G GrpHom H ) -> ran F e. ( SubGrp ` H ) )
10	8 9	syl	|- ( G e. Grp -> ran F e. ( SubGrp ` H ) )
11	5 10	eqeltrid	|- ( G e. Grp -> S e. ( SubGrp ` H ) )
12	5	eqimss2i	|- ran F C_ S
13		eqid	|- ( H |`s S ) = ( H |`s S )
14	13	resghm2b	|- ( ( S e. ( SubGrp ` H ) /\ ran F C_ S ) -> ( F e. ( G GrpHom H ) <-> F e. ( G GrpHom ( H |`s S ) ) ) )
15	11 12 14	sylancl	|- ( G e. Grp -> ( F e. ( G GrpHom H ) <-> F e. ( G GrpHom ( H |`s S ) ) ) )
16	8 15	mpbid	|- ( G e. Grp -> F e. ( G GrpHom ( H |`s S ) ) )
17	1 3 6 2 7 4	cayleylem2	|- ( G e. Grp -> F : X -1-1-> ( Base ` H ) )
18		f1f1orn	|- ( F : X -1-1-> ( Base ` H ) -> F : X -1-1-onto-> ran F )
19	17 18	syl	|- ( G e. Grp -> F : X -1-1-onto-> ran F )
20		f1oeq3	|- ( S = ran F -> ( F : X -1-1-onto-> S <-> F : X -1-1-onto-> ran F ) )
21	5 20	ax-mp	|- ( F : X -1-1-onto-> S <-> F : X -1-1-onto-> ran F )
22	19 21	sylibr	|- ( G e. Grp -> F : X -1-1-onto-> S )
23	11 16 22	3jca	|- ( G e. Grp -> ( S e. ( SubGrp ` H ) /\ F e. ( G GrpHom ( H |`s S ) ) /\ F : X -1-1-onto-> S ) )