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	⊢ 𝑋 = ( Base ‘ 𝐺 )
	cayley.h	⊢ 𝐻 = ( SymGrp ‘ 𝑋 )
	cayley.p	⊢ + = ( +g ‘ 𝐺 )
	cayley.f	⊢ 𝐹 = ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 + 𝑎 ) ) )
	cayley.s	⊢ 𝑆 = ran 𝐹
Assertion	cayley	⊢ ( 𝐺 ∈ Grp → ( 𝑆 ∈ ( SubGrp ‘ 𝐻 ) ∧ 𝐹 ∈ ( 𝐺 GrpHom ( 𝐻 ↾s 𝑆 ) ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		cayley.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		cayley.h	⊢ 𝐻 = ( SymGrp ‘ 𝑋 )
3		cayley.p	⊢ + = ( +g ‘ 𝐺 )
4		cayley.f	⊢ 𝐹 = ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 + 𝑎 ) ) )
5		cayley.s	⊢ 𝑆 = ran 𝐹
6		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
7		eqid	⊢ ( Base ‘ 𝐻 ) = ( Base ‘ 𝐻 )
8	1 3 6 2 7 4	cayleylem1	⊢ ( 𝐺 ∈ Grp → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
9		ghmrn	⊢ ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) → ran 𝐹 ∈ ( SubGrp ‘ 𝐻 ) )
10	8 9	syl	⊢ ( 𝐺 ∈ Grp → ran 𝐹 ∈ ( SubGrp ‘ 𝐻 ) )
11	5 10	eqeltrid	⊢ ( 𝐺 ∈ Grp → 𝑆 ∈ ( SubGrp ‘ 𝐻 ) )
12	5	eqimss2i	⊢ ran 𝐹 ⊆ 𝑆
13		eqid	⊢ ( 𝐻 ↾s 𝑆 ) = ( 𝐻 ↾s 𝑆 )
14	13	resghm2b	⊢ ( ( 𝑆 ∈ ( SubGrp ‘ 𝐻 ) ∧ ran 𝐹 ⊆ 𝑆 ) → ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ↔ 𝐹 ∈ ( 𝐺 GrpHom ( 𝐻 ↾s 𝑆 ) ) ) )
15	11 12 14	sylancl	⊢ ( 𝐺 ∈ Grp → ( 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) ↔ 𝐹 ∈ ( 𝐺 GrpHom ( 𝐻 ↾s 𝑆 ) ) ) )
16	8 15	mpbid	⊢ ( 𝐺 ∈ Grp → 𝐹 ∈ ( 𝐺 GrpHom ( 𝐻 ↾s 𝑆 ) ) )
17	1 3 6 2 7 4	cayleylem2	⊢ ( 𝐺 ∈ Grp → 𝐹 : 𝑋 –1-1→ ( Base ‘ 𝐻 ) )
18		f1f1orn	⊢ ( 𝐹 : 𝑋 –1-1→ ( Base ‘ 𝐻 ) → 𝐹 : 𝑋 –1-1-onto→ ran 𝐹 )
19	17 18	syl	⊢ ( 𝐺 ∈ Grp → 𝐹 : 𝑋 –1-1-onto→ ran 𝐹 )
20		f1oeq3	⊢ ( 𝑆 = ran 𝐹 → ( 𝐹 : 𝑋 –1-1-onto→ 𝑆 ↔ 𝐹 : 𝑋 –1-1-onto→ ran 𝐹 ) )
21	5 20	ax-mp	⊢ ( 𝐹 : 𝑋 –1-1-onto→ 𝑆 ↔ 𝐹 : 𝑋 –1-1-onto→ ran 𝐹 )
22	19 21	sylibr	⊢ ( 𝐺 ∈ Grp → 𝐹 : 𝑋 –1-1-onto→ 𝑆 )
23	11 16 22	3jca	⊢ ( 𝐺 ∈ Grp → ( 𝑆 ∈ ( SubGrp ‘ 𝐻 ) ∧ 𝐹 ∈ ( 𝐺 GrpHom ( 𝐻 ↾s 𝑆 ) ) ∧ 𝐹 : 𝑋 –1-1-onto→ 𝑆 ) )