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 ⊢ 𝑋 = ( Base ‘ 𝐺 )
cayley.h ⊢ 𝐻 = ( SymGrp ‘ 𝑋 )
Assertion cayleyth ( 𝐺 ∈ Grp → ∃ 𝑠 ∈ ( SubGrp ‘ 𝐻 ) ∃ 𝑓 ∈ ( 𝐺 GrpHom ( 𝐻 ↾s 𝑠 ) ) 𝑓 : 𝑋 –1-1-onto→ 𝑠 )

Proof

Step Hyp Ref Expression
1 cayley.x ⊢ 𝑋 = ( Base ‘ 𝐺 )
2 cayley.h ⊢ 𝐻 = ( SymGrp ‘ 𝑋 )
3 eqid ⊢ ( +g ‘ 𝐺 ) = ( +g ‘ 𝐺 )
4 eqid ⊢ ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) ) = ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) )
5 eqid ⊢ ran ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) ) = ran ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) )
6 1 2 3 4 5 cayley ⊢ ( 𝐺 ∈ Grp → ( ran ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) ) ∈ ( SubGrp ‘ 𝐻 ) ∧ ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) ) ∈ ( 𝐺 GrpHom ( 𝐻 ↾s ran ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) ) ) ) ∧ ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) ) : 𝑋 –1-1-onto→ ran ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) ) ) )
7 6 simp1d ⊢ ( 𝐺 ∈ Grp → ran ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) ) ∈ ( SubGrp ‘ 𝐻 ) )
8 6 simp2d ⊢ ( 𝐺 ∈ Grp → ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) ) ∈ ( 𝐺 GrpHom ( 𝐻 ↾s ran ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) ) ) ) )
9 6 simp3d ⊢ ( 𝐺 ∈ Grp → ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) ) : 𝑋 –1-1-onto→ ran ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) ) )
10 f1oeq1 ⊢ ( 𝑓 = ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) ) → ( 𝑓 : 𝑋 –1-1-onto→ ran ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) ) ↔ ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) ) : 𝑋 –1-1-onto→ ran ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) ) ) )
11 10 rspcev ⊢ ( ( ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) ) ∈ ( 𝐺 GrpHom ( 𝐻 ↾s ran ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) ) ) ) ∧ ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) ) : 𝑋 –1-1-onto→ ran ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) ) ) → ∃ 𝑓 ∈ ( 𝐺 GrpHom ( 𝐻 ↾s ran ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) ) ) ) 𝑓 : 𝑋 –1-1-onto→ ran ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) ) )
12 8 9 11 syl2anc ⊢ ( 𝐺 ∈ Grp → ∃ 𝑓 ∈ ( 𝐺 GrpHom ( 𝐻 ↾s ran ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) ) ) ) 𝑓 : 𝑋 –1-1-onto→ ran ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) ) )
13 oveq2 ⊢ ( 𝑠 = ran ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) ) → ( 𝐻 ↾s 𝑠 ) = ( 𝐻 ↾s ran ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) ) ) )
14 13 oveq2d ⊢ ( 𝑠 = ran ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) ) → ( 𝐺 GrpHom ( 𝐻 ↾s 𝑠 ) ) = ( 𝐺 GrpHom ( 𝐻 ↾s ran ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) ) ) ) )
15 f1oeq3 ⊢ ( 𝑠 = ran ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) ) → ( 𝑓 : 𝑋 –1-1-onto→ 𝑠 ↔ 𝑓 : 𝑋 –1-1-onto→ ran ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) ) ) )
16 14 15 rexeqbidv ⊢ ( 𝑠 = ran ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) ) → ( ∃ 𝑓 ∈ ( 𝐺 GrpHom ( 𝐻 ↾s 𝑠 ) ) 𝑓 : 𝑋 –1-1-onto→ 𝑠 ↔ ∃ 𝑓 ∈ ( 𝐺 GrpHom ( 𝐻 ↾s ran ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) ) ) ) 𝑓 : 𝑋 –1-1-onto→ ran ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) ) ) )
17 16 rspcev ⊢ ( ( ran ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) ) ∈ ( SubGrp ‘ 𝐻 ) ∧ ∃ 𝑓 ∈ ( 𝐺 GrpHom ( 𝐻 ↾s ran ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) ) ) ) 𝑓 : 𝑋 –1-1-onto→ ran ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( +g ‘ 𝐺 ) 𝑎 ) ) ) ) → ∃ 𝑠 ∈ ( SubGrp ‘ 𝐻 ) ∃ 𝑓 ∈ ( 𝐺 GrpHom ( 𝐻 ↾s 𝑠 ) ) 𝑓 : 𝑋 –1-1-onto→ 𝑠 )
18 7 12 17 syl2anc ⊢ ( 𝐺 ∈ Grp → ∃ 𝑠 ∈ ( SubGrp ‘ 𝐻 ) ∃ 𝑓 ∈ ( 𝐺 GrpHom ( 𝐻 ↾s 𝑠 ) ) 𝑓 : 𝑋 –1-1-onto→ 𝑠 )