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	$⊢ \underset{˙}{+} = +_{G}$
	cayley.f	$⊢ F = (g \in X ⟼ (a \in X ⟼ g \underset{˙}{+} a))$
	cayley.s	$⊢ S = ran F$
Assertion	cayley	$⊢ G \in Grp \to (S \in SubGrp (H) \land F \in (G GrpHom (H ↾_{𝑠} S)) \land F : X \underset{1-1 onto}{⟶} S)$

Proof

Step	Hyp	Ref	Expression
1		cayley.x	$⊢ X = {Base}_{G}$
2		cayley.h	$⊢ H = SymGrp (X)$
3		cayley.p	$⊢ \underset{˙}{+} = +_{G}$
4		cayley.f	$⊢ F = (g \in X ⟼ (a \in X ⟼ g \underset{˙}{+} 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 \in Grp \to F \in (G GrpHom H)$
9		ghmrn	$⊢ F \in (G GrpHom H) \to ran F \in SubGrp (H)$
10	8 9	syl	$⊢ G \in Grp \to ran F \in SubGrp (H)$
11	5 10	eqeltrid	$⊢ G \in Grp \to S \in SubGrp (H)$
12	5	eqimss2i	$⊢ ran F \subseteq S$
13		eqid	$⊢ H ↾_{𝑠} S = H ↾_{𝑠} S$
14	13	resghm2b	$⊢ (S \in SubGrp (H) \land ran F \subseteq S) \to (F \in (G GrpHom H) \leftrightarrow F \in (G GrpHom (H ↾_{𝑠} S)))$
15	11 12 14	sylancl	$⊢ G \in Grp \to (F \in (G GrpHom H) \leftrightarrow F \in (G GrpHom (H ↾_{𝑠} S)))$
16	8 15	mpbid	$⊢ G \in Grp \to F \in (G GrpHom (H ↾_{𝑠} S))$
17	1 3 6 2 7 4	cayleylem2	$⊢ G \in Grp \to F : X \underset{1-1}{⟶} {Base}_{H}$
18		f1f1orn	$⊢ F : X \underset{1-1}{⟶} {Base}_{H} \to F : X \underset{1-1 onto}{⟶} ran F$
19	17 18	syl	$⊢ G \in Grp \to F : X \underset{1-1 onto}{⟶} ran F$
20		f1oeq3	$⊢ S = ran F \to (F : X \underset{1-1 onto}{⟶} S \leftrightarrow F : X \underset{1-1 onto}{⟶} ran F)$
21	5 20	ax-mp	$⊢ F : X \underset{1-1 onto}{⟶} S \leftrightarrow F : X \underset{1-1 onto}{⟶} ran F$
22	19 21	sylibr	$⊢ G \in Grp \to F : X \underset{1-1 onto}{⟶} S$
23	11 16 22	3jca	$⊢ G \in Grp \to (S \in SubGrp (H) \land F \in (G GrpHom (H ↾_{𝑠} S)) \land F : X \underset{1-1 onto}{⟶} S)$

Metamath Proof Explorer

Theorem cayley

Proof