Theorem cayleylem1

Description: Lemma for cayley . (Contributed by Paul Chapman, 3-Mar-2008) (Revised by Mario Carneiro, 13-Jan-2015)

	Ref	Expression
Hypotheses	cayleylem1.x	$$⊢X={\mathrm{Base}}_G$$
	cayleylem1.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	cayleylem1.u	$$⊢\underset{\dot{}}{0}=0_G$$
	cayleylem1.h	$$⊢H=\mathrm{SymGrp}\left(X\right)$$
	cayleylem1.s	$$⊢S={\mathrm{Base}}_H$$
	cayleylem1.f	$$⊢F=\left(g\in X⟼\left(a\in X⟼g\underset{\dot{}}{+}a\right)\right)$$
Assertion	cayleylem1	$$⊢G\in \mathrm{Grp}\to F\in \left(G\mathrm{GrpHom}H\right)$$

Proof

Step	Hyp	Ref	Expression
1		cayleylem1.x	$$⊢X={\mathrm{Base}}_G$$
2		cayleylem1.p	$$⊢\underset{\dot{}}{+}={+}_G$$
3		cayleylem1.u	$$⊢\underset{\dot{}}{0}=0_G$$
4		cayleylem1.h	$$⊢H=\mathrm{SymGrp}\left(X\right)$$
5		cayleylem1.s	$$⊢S={\mathrm{Base}}_H$$
6		cayleylem1.f	$$⊢F=\left(g\in X⟼\left(a\in X⟼g\underset{\dot{}}{+}a\right)\right)$$
7		eqid	$$⊢\left(x\in X,y\in X⟼x\underset{\dot{}}{+}y\right)=\left(x\in X,y\in X⟼x\underset{\dot{}}{+}y\right)$$
8	1 2 7	gaid2	$$⊢G\in \mathrm{Grp}\to \left(x\in X,y\in X⟼x\underset{\dot{}}{+}y\right)\in \left(G\mathrm{GrpAct}X\right)$$
9		oveq12	$$⊢\left(x=g\wedge y=a\right)\to x\underset{\dot{}}{+}y=g\underset{\dot{}}{+}a$$
10		ovex	$$⊢g\underset{\dot{}}{+}a\in \mathrm{V}$$
11	9 7 10	ovmpoa	$$⊢\left(g\in X\wedge a\in X\right)\to g\left(x\in X,y\in X⟼x\underset{\dot{}}{+}y\right)a=g\underset{\dot{}}{+}a$$
12	11	mpteq2dva	$$⊢g\in X\to \left(a\in X⟼g\left(x\in X,y\in X⟼x\underset{\dot{}}{+}y\right)a\right)=\left(a\in X⟼g\underset{\dot{}}{+}a\right)$$
13	12	mpteq2ia	$$⊢\left(g\in X⟼\left(a\in X⟼g\left(x\in X,y\in X⟼x\underset{\dot{}}{+}y\right)a\right)\right)=\left(g\in X⟼\left(a\in X⟼g\underset{\dot{}}{+}a\right)\right)$$
14	6 13	eqtr4i	$$⊢F=\left(g\in X⟼\left(a\in X⟼g\left(x\in X,y\in X⟼x\underset{\dot{}}{+}y\right)a\right)\right)$$
15	1 4 14	galactghm	$$⊢\left(x\in X,y\in X⟼x\underset{\dot{}}{+}y\right)\in \left(G\mathrm{GrpAct}X\right)\to F\in \left(G\mathrm{GrpHom}H\right)$$
16	8 15	syl	$$⊢G\in \mathrm{Grp}\to F\in \left(G\mathrm{GrpHom}H\right)$$