Metamath Proof Explorer

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
cayley.f ⊢ F = g ∈ X ⟼ a ∈ X ⟼ g + ˙ a
cayley.s ⊢ S = ran ⁡ F
Assertion cayley ⊢ G ∈ Grp → S ∈ SubGrp ⁡ H ∧ F ∈ G GrpHom H ↾ 𝑠 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
4 cayley.f ⊢ F = g ∈ X ⟼ a ∈ X ⟼ g + ˙ a
5 cayley.s ⊢ S = ran ⁡ F
6 eqid ⊢ 0 G = 0 G
7 eqid ⊢ Base H = Base H
8 1 3 6 2 7 4 cayleylem1 ⊢ G ∈ Grp → F ∈ G GrpHom H
9 ghmrn ⊢ F ∈ G GrpHom H → ran ⁡ F ∈ SubGrp ⁡ H
10 8 9 syl ⊢ G ∈ Grp → ran ⁡ F ∈ SubGrp ⁡ H
11 5 10 eqeltrid ⊢ G ∈ Grp → S ∈ SubGrp ⁡ H
12 5 eqimss2i ⊢ ran ⁡ F ⊆ S
13 eqid ⊢ H ↾ 𝑠 S = H ↾ 𝑠 S
14 13 resghm2b ⊢ S ∈ SubGrp ⁡ H ∧ ran ⁡ F ⊆ S → F ∈ G GrpHom H ↔ F ∈ G GrpHom H ↾ 𝑠 S
15 11 12 14 sylancl ⊢ G ∈ Grp → F ∈ G GrpHom H ↔ F ∈ G GrpHom H ↾ 𝑠 S
16 8 15 mpbid ⊢ G ∈ Grp → F ∈ G GrpHom H ↾ 𝑠 S
17 1 3 6 2 7 4 cayleylem2 ⊢ G ∈ 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 ∈ 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 ∈ Grp → F : X ⟶ 1-1 onto S
23 11 16 22 3jca ⊢ G ∈ Grp → S ∈ SubGrp ⁡ H ∧ F ∈ G GrpHom H ↾ 𝑠 S ∧ F : X ⟶ 1-1 onto S