Theorem sylow3lem5

Description: Lemma for sylow3 , second part. Reduce the group action of sylow3lem1 to a given Sylow subgroup. (Contributed by Mario Carneiro, 19-Jan-2015)

	Ref	Expression
Hypotheses	sylow3.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
	sylow3.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
	sylow3.xf	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	sylow3.p	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
	sylow3lem5.a	⊢ + = ( +g ‘ 𝐺 )
	sylow3lem5.d	⊢ − = ( -g ‘ 𝐺 )
	sylow3lem5.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) )
	sylow3lem5.m	⊢ ⊕ = ( 𝑥 ∈ 𝐾 , 𝑦 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) )
Assertion	sylow3lem5	⊢ ( 𝜑 → ⊕ ∈ ( ( 𝐺 ↾s 𝐾 ) GrpAct ( 𝑃 pSyl 𝐺 ) ) )

Proof

Step	Hyp	Ref	Expression
1		sylow3.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		sylow3.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
3		sylow3.xf	⊢ ( 𝜑 → 𝑋 ∈ Fin )
4		sylow3.p	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
5		sylow3lem5.a	⊢ + = ( +g ‘ 𝐺 )
6		sylow3lem5.d	⊢ − = ( -g ‘ 𝐺 )
7		sylow3lem5.k	⊢ ( 𝜑 → 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) )
8		sylow3lem5.m	⊢ ⊕ = ( 𝑥 ∈ 𝐾 , 𝑦 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) )
9		slwsubg	⊢ ( 𝐾 ∈ ( 𝑃 pSyl 𝐺 ) → 𝐾 ∈ ( SubGrp ‘ 𝐺 ) )
10	7 9	syl	⊢ ( 𝜑 → 𝐾 ∈ ( SubGrp ‘ 𝐺 ) )
11	1	subgss	⊢ ( 𝐾 ∈ ( SubGrp ‘ 𝐺 ) → 𝐾 ⊆ 𝑋 )
12	10 11	syl	⊢ ( 𝜑 → 𝐾 ⊆ 𝑋 )
13		ssid	⊢ ( 𝑃 pSyl 𝐺 ) ⊆ ( 𝑃 pSyl 𝐺 )
14		resmpo	⊢ ( ( 𝐾 ⊆ 𝑋 ∧ ( 𝑃 pSyl 𝐺 ) ⊆ ( 𝑃 pSyl 𝐺 ) ) → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) ) ↾ ( 𝐾 × ( 𝑃 pSyl 𝐺 ) ) ) = ( 𝑥 ∈ 𝐾 , 𝑦 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) ) )
15	12 13 14	sylancl	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) ) ↾ ( 𝐾 × ( 𝑃 pSyl 𝐺 ) ) ) = ( 𝑥 ∈ 𝐾 , 𝑦 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) ) )
16	15 8	eqtr4di	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) ) ↾ ( 𝐾 × ( 𝑃 pSyl 𝐺 ) ) ) = ⊕ )
17		oveq2	⊢ ( 𝑧 = 𝑐 → ( 𝑥 + 𝑧 ) = ( 𝑥 + 𝑐 ) )
18	17	oveq1d	⊢ ( 𝑧 = 𝑐 → ( ( 𝑥 + 𝑧 ) − 𝑥 ) = ( ( 𝑥 + 𝑐 ) − 𝑥 ) )
19	18	cbvmptv	⊢ ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) = ( 𝑐 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑐 ) − 𝑥 ) )
20		oveq1	⊢ ( 𝑥 = 𝑎 → ( 𝑥 + 𝑐 ) = ( 𝑎 + 𝑐 ) )
21		id	⊢ ( 𝑥 = 𝑎 → 𝑥 = 𝑎 )
22	20 21	oveq12d	⊢ ( 𝑥 = 𝑎 → ( ( 𝑥 + 𝑐 ) − 𝑥 ) = ( ( 𝑎 + 𝑐 ) − 𝑎 ) )
23	22	mpteq2dv	⊢ ( 𝑥 = 𝑎 → ( 𝑐 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑐 ) − 𝑥 ) ) = ( 𝑐 ∈ 𝑦 ↦ ( ( 𝑎 + 𝑐 ) − 𝑎 ) ) )
24	19 23	eqtrid	⊢ ( 𝑥 = 𝑎 → ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) = ( 𝑐 ∈ 𝑦 ↦ ( ( 𝑎 + 𝑐 ) − 𝑎 ) ) )
25	24	rneqd	⊢ ( 𝑥 = 𝑎 → ran ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) = ran ( 𝑐 ∈ 𝑦 ↦ ( ( 𝑎 + 𝑐 ) − 𝑎 ) ) )
26		mpteq1	⊢ ( 𝑦 = 𝑏 → ( 𝑐 ∈ 𝑦 ↦ ( ( 𝑎 + 𝑐 ) − 𝑎 ) ) = ( 𝑐 ∈ 𝑏 ↦ ( ( 𝑎 + 𝑐 ) − 𝑎 ) ) )
27	26	rneqd	⊢ ( 𝑦 = 𝑏 → ran ( 𝑐 ∈ 𝑦 ↦ ( ( 𝑎 + 𝑐 ) − 𝑎 ) ) = ran ( 𝑐 ∈ 𝑏 ↦ ( ( 𝑎 + 𝑐 ) − 𝑎 ) ) )
28	25 27	cbvmpov	⊢ ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) ) = ( 𝑎 ∈ 𝑋 , 𝑏 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑐 ∈ 𝑏 ↦ ( ( 𝑎 + 𝑐 ) − 𝑎 ) ) )
29	1 2 3 4 5 6 28	sylow3lem1	⊢ ( 𝜑 → ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) ) ∈ ( 𝐺 GrpAct ( 𝑃 pSyl 𝐺 ) ) )
30		eqid	⊢ ( 𝐺 ↾s 𝐾 ) = ( 𝐺 ↾s 𝐾 )
31	30	gasubg	⊢ ( ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) ) ∈ ( 𝐺 GrpAct ( 𝑃 pSyl 𝐺 ) ) ∧ 𝐾 ∈ ( SubGrp ‘ 𝐺 ) ) → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) ) ↾ ( 𝐾 × ( 𝑃 pSyl 𝐺 ) ) ) ∈ ( ( 𝐺 ↾s 𝐾 ) GrpAct ( 𝑃 pSyl 𝐺 ) ) )
32	29 10 31	syl2anc	⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑋 , 𝑦 ∈ ( 𝑃 pSyl 𝐺 ) ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( ( 𝑥 + 𝑧 ) − 𝑥 ) ) ) ↾ ( 𝐾 × ( 𝑃 pSyl 𝐺 ) ) ) ∈ ( ( 𝐺 ↾s 𝐾 ) GrpAct ( 𝑃 pSyl 𝐺 ) ) )
33	16 32	eqeltrrd	⊢ ( 𝜑 → ⊕ ∈ ( ( 𝐺 ↾s 𝐾 ) GrpAct ( 𝑃 pSyl 𝐺 ) ) )