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	⊢ 𝑋 = ( Base ‘ 𝐺 )
	cayleylem1.p	⊢ + = ( +g ‘ 𝐺 )
	cayleylem1.u	⊢ 0 = ( 0g ‘ 𝐺 )
	cayleylem1.h	⊢ 𝐻 = ( SymGrp ‘ 𝑋 )
	cayleylem1.s	⊢ 𝑆 = ( Base ‘ 𝐻 )
	cayleylem1.f	⊢ 𝐹 = ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 + 𝑎 ) ) )
Assertion	cayleylem1	⊢ ( 𝐺 ∈ Grp → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )

Proof

Step	Hyp	Ref	Expression
1		cayleylem1.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		cayleylem1.p	⊢ + = ( +g ‘ 𝐺 )
3		cayleylem1.u	⊢ 0 = ( 0g ‘ 𝐺 )
4		cayleylem1.h	⊢ 𝐻 = ( SymGrp ‘ 𝑋 )
5		cayleylem1.s	⊢ 𝑆 = ( Base ‘ 𝐻 )
6		cayleylem1.f	⊢ 𝐹 = ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 + 𝑎 ) ) )
7		eqid	⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 + 𝑦 ) ) = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 + 𝑦 ) )
8	1 2 7	gaid2	⊢ ( 𝐺 ∈ Grp → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 + 𝑦 ) ) ∈ ( 𝐺 GrpAct 𝑋 ) )
9		oveq12	⊢ ( ( 𝑥 = 𝑔 ∧ 𝑦 = 𝑎 ) → ( 𝑥 + 𝑦 ) = ( 𝑔 + 𝑎 ) )
10		ovex	⊢ ( 𝑔 + 𝑎 ) ∈ V
11	9 7 10	ovmpoa	⊢ ( ( 𝑔 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋 ) → ( 𝑔 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 + 𝑦 ) ) 𝑎 ) = ( 𝑔 + 𝑎 ) )
12	11	mpteq2dva	⊢ ( 𝑔 ∈ 𝑋 → ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 + 𝑦 ) ) 𝑎 ) ) = ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 + 𝑎 ) ) )
13	12	mpteq2ia	⊢ ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 + 𝑦 ) ) 𝑎 ) ) ) = ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 + 𝑎 ) ) )
14	6 13	eqtr4i	⊢ 𝐹 = ( 𝑔 ∈ 𝑋 ↦ ( 𝑎 ∈ 𝑋 ↦ ( 𝑔 ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 + 𝑦 ) ) 𝑎 ) ) )
15	1 4 14	galactghm	⊢ ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( 𝑥 + 𝑦 ) ) ∈ ( 𝐺 GrpAct 𝑋 ) → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )
16	8 15	syl	⊢ ( 𝐺 ∈ Grp → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )