Metamath Proof Explorer

Theorem cayleyth

Description: Cayley's Theorem (existence version): every group G is isomorphic to a subgroup of the symmetric group on the underlying set of G . (For any group G there exists an isomorphism f between G and a subgroup h of the symmetric group on the underlying set of G .) See also Theorem 3.15 in Rotman p. 42. (Contributed by Paul Chapman, 3-Mar-2008) (Revised by Mario Carneiro, 13-Jan-2015)

Ref Expression
Hypotheses cayley.x ⊢ X = Base G
cayley.h ⊢ H = SymGrp ⁡ X
Assertion cayleyth ⊢ 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 eqid ⊢ + G = + G
4 eqid ⊢ g ∈ X ⟼ a ∈ X ⟼ g + G a = g ∈ X ⟼ a ∈ X ⟼ g + G a
5 eqid ⊢ ran ⁡ g ∈ X ⟼ a ∈ X ⟼ g + G a = ran ⁡ g ∈ X ⟼ a ∈ X ⟼ g + G a
6 1 2 3 4 5 cayley ⊢ G ∈ Grp → ran ⁡ g ∈ X ⟼ a ∈ X ⟼ g + G a ∈ SubGrp ⁡ H ∧ g ∈ X ⟼ a ∈ X ⟼ g + G a ∈ G GrpHom H ↾ 𝑠 ran ⁡ g ∈ X ⟼ a ∈ X ⟼ g + G a ∧ g ∈ X ⟼ a ∈ X ⟼ g + G a : X ⟶ 1-1 onto ran ⁡ g ∈ X ⟼ a ∈ X ⟼ g + G a
7 6 simp1d ⊢ G ∈ Grp → ran ⁡ g ∈ X ⟼ a ∈ X ⟼ g + G a ∈ SubGrp ⁡ H
8 6 simp2d ⊢ G ∈ Grp → g ∈ X ⟼ a ∈ X ⟼ g + G a ∈ G GrpHom H ↾ 𝑠 ran ⁡ g ∈ X ⟼ a ∈ X ⟼ g + G a
9 6 simp3d ⊢ G ∈ Grp → g ∈ X ⟼ a ∈ X ⟼ g + G a : X ⟶ 1-1 onto ran ⁡ g ∈ X ⟼ a ∈ X ⟼ g + G a
10 f1oeq1 ⊢ f = g ∈ X ⟼ a ∈ X ⟼ g + G a → f : X ⟶ 1-1 onto ran ⁡ g ∈ X ⟼ a ∈ X ⟼ g + G a ↔ g ∈ X ⟼ a ∈ X ⟼ g + G a : X ⟶ 1-1 onto ran ⁡ g ∈ X ⟼ a ∈ X ⟼ g + G a
11 10 rspcev ⊢ g ∈ X ⟼ a ∈ X ⟼ g + G a ∈ G GrpHom H ↾ 𝑠 ran ⁡ g ∈ X ⟼ a ∈ X ⟼ g + G a ∧ g ∈ X ⟼ a ∈ X ⟼ g + G a : X ⟶ 1-1 onto ran ⁡ g ∈ X ⟼ a ∈ X ⟼ g + G a → ∃ f ∈ G GrpHom H ↾ 𝑠 ran ⁡ g ∈ X ⟼ a ∈ X ⟼ g + G a f : X ⟶ 1-1 onto ran ⁡ g ∈ X ⟼ a ∈ X ⟼ g + G a
12 8 9 11 syl2anc ⊢ G ∈ Grp → ∃ f ∈ G GrpHom H ↾ 𝑠 ran ⁡ g ∈ X ⟼ a ∈ X ⟼ g + G a f : X ⟶ 1-1 onto ran ⁡ g ∈ X ⟼ a ∈ X ⟼ g + G a
13 oveq2 ⊢ s = ran ⁡ g ∈ X ⟼ a ∈ X ⟼ g + G a → H ↾ 𝑠 s = H ↾ 𝑠 ran ⁡ g ∈ X ⟼ a ∈ X ⟼ g + G a
14 13 oveq2d ⊢ s = ran ⁡ g ∈ X ⟼ a ∈ X ⟼ g + G a → G GrpHom H ↾ 𝑠 s = G GrpHom H ↾ 𝑠 ran ⁡ g ∈ X ⟼ a ∈ X ⟼ g + G a
15 f1oeq3 ⊢ s = ran ⁡ g ∈ X ⟼ a ∈ X ⟼ g + G a → f : X ⟶ 1-1 onto s ↔ f : X ⟶ 1-1 onto ran ⁡ g ∈ X ⟼ a ∈ X ⟼ g + G a
16 14 15 rexeqbidv ⊢ s = ran ⁡ g ∈ X ⟼ a ∈ X ⟼ g + G a → ∃ f ∈ G GrpHom H ↾ 𝑠 s f : X ⟶ 1-1 onto s ↔ ∃ f ∈ G GrpHom H ↾ 𝑠 ran ⁡ g ∈ X ⟼ a ∈ X ⟼ g + G a f : X ⟶ 1-1 onto ran ⁡ g ∈ X ⟼ a ∈ X ⟼ g + G a
17 16 rspcev ⊢ ran ⁡ g ∈ X ⟼ a ∈ X ⟼ g + G a ∈ SubGrp ⁡ H ∧ ∃ f ∈ G GrpHom H ↾ 𝑠 ran ⁡ g ∈ X ⟼ a ∈ X ⟼ g + G a f : X ⟶ 1-1 onto ran ⁡ g ∈ X ⟼ a ∈ X ⟼ g + G a → ∃ s ∈ SubGrp ⁡ H ∃ f ∈ G GrpHom H ↾ 𝑠 s f : X ⟶ 1-1 onto s
18 7 12 17 syl2anc ⊢ G ∈ Grp → ∃ s ∈ SubGrp ⁡ H ∃ f ∈ G GrpHom H ↾ 𝑠 s f : X ⟶ 1-1 onto s