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	$$⊢X={\mathrm{Base}}_G$$
	sylow3.g	$$⊢\phi \to G\in \mathrm{Grp}$$
	sylow3.xf	$$⊢\phi \to X\in \mathrm{Fin}$$
	sylow3.p	$$⊢\phi \to P\in \mathbb{P}$$
	sylow3lem5.a	$$⊢\underset{\dot{}}{+}={+}_G$$
	sylow3lem5.d	$$⊢\underset{\dot{}}{-}={-}_G$$
	sylow3lem5.k	$$⊢\phi \to K\in \left(P\mathrm{pSyl}G\right)$$
	sylow3lem5.m	$$⊢\underset{\dot{}}{\oplus }=\left(x\in K,y\in \left(P\mathrm{pSyl}G\right)⟼\mathrm{ran}\left(z\in y⟼\left(x\underset{\dot{}}{+}z\right)\underset{\dot{}}{-}x\right)\right)$$
Assertion	sylow3lem5	$$⊢\phi \to \underset{\dot{}}{\oplus }\in \left(\left(G{\upharpoonright }_{𝑠}K\right)\mathrm{GrpAct}\left(P\mathrm{pSyl}G\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		sylow3.x	$$⊢X={\mathrm{Base}}_G$$
2		sylow3.g	$$⊢\phi \to G\in \mathrm{Grp}$$
3		sylow3.xf	$$⊢\phi \to X\in \mathrm{Fin}$$
4		sylow3.p	$$⊢\phi \to P\in \mathbb{P}$$
5		sylow3lem5.a	$$⊢\underset{\dot{}}{+}={+}_G$$
6		sylow3lem5.d	$$⊢\underset{\dot{}}{-}={-}_G$$
7		sylow3lem5.k	$$⊢\phi \to K\in \left(P\mathrm{pSyl}G\right)$$
8		sylow3lem5.m	$$⊢\underset{\dot{}}{\oplus }=\left(x\in K,y\in \left(P\mathrm{pSyl}G\right)⟼\mathrm{ran}\left(z\in y⟼\left(x\underset{\dot{}}{+}z\right)\underset{\dot{}}{-}x\right)\right)$$
9		slwsubg	$$⊢K\in \left(P\mathrm{pSyl}G\right)\to K\in \mathrm{SubGrp}\left(G\right)$$
10	7 9	syl	$$⊢\phi \to K\in \mathrm{SubGrp}\left(G\right)$$
11	1	subgss	$$⊢K\in \mathrm{SubGrp}\left(G\right)\to K\subseteq X$$
12	10 11	syl	$$⊢\phi \to K\subseteq X$$
13		ssid	$$⊢P\mathrm{pSyl}G\subseteq P\mathrm{pSyl}G$$
14		resmpo	$$⊢\left(K\subseteq X\wedge P\mathrm{pSyl}G\subseteq P\mathrm{pSyl}G\right)\to {\left(x\in X,y\in \left(P\mathrm{pSyl}G\right)⟼\mathrm{ran}\left(z\in y⟼\left(x\underset{\dot{}}{+}z\right)\underset{\dot{}}{-}x\right)\right)\upharpoonright }_{\left(K\times \left(P\mathrm{pSyl}G\right)\right)}=\left(x\in K,y\in \left(P\mathrm{pSyl}G\right)⟼\mathrm{ran}\left(z\in y⟼\left(x\underset{\dot{}}{+}z\right)\underset{\dot{}}{-}x\right)\right)$$
15	12 13 14	sylancl	$$⊢\phi \to {\left(x\in X,y\in \left(P\mathrm{pSyl}G\right)⟼\mathrm{ran}\left(z\in y⟼\left(x\underset{\dot{}}{+}z\right)\underset{\dot{}}{-}x\right)\right)\upharpoonright }_{\left(K\times \left(P\mathrm{pSyl}G\right)\right)}=\left(x\in K,y\in \left(P\mathrm{pSyl}G\right)⟼\mathrm{ran}\left(z\in y⟼\left(x\underset{\dot{}}{+}z\right)\underset{\dot{}}{-}x\right)\right)$$
16	15 8	syl6eqr	$$⊢\phi \to {\left(x\in X,y\in \left(P\mathrm{pSyl}G\right)⟼\mathrm{ran}\left(z\in y⟼\left(x\underset{\dot{}}{+}z\right)\underset{\dot{}}{-}x\right)\right)\upharpoonright }_{\left(K\times \left(P\mathrm{pSyl}G\right)\right)}=\underset{\dot{}}{\oplus }$$
17		oveq2	$$⊢z=c\to x\underset{\dot{}}{+}z=x\underset{\dot{}}{+}c$$
18	17	oveq1d	$$⊢z=c\to \left(x\underset{\dot{}}{+}z\right)\underset{\dot{}}{-}x=\left(x\underset{\dot{}}{+}c\right)\underset{\dot{}}{-}x$$
19	18	cbvmptv	$$⊢\left(z\in y⟼\left(x\underset{\dot{}}{+}z\right)\underset{\dot{}}{-}x\right)=\left(c\in y⟼\left(x\underset{\dot{}}{+}c\right)\underset{\dot{}}{-}x\right)$$
20		oveq1	$$⊢x=a\to x\underset{\dot{}}{+}c=a\underset{\dot{}}{+}c$$
21		id	$$⊢x=a\to x=a$$
22	20 21	oveq12d	$$⊢x=a\to \left(x\underset{\dot{}}{+}c\right)\underset{\dot{}}{-}x=\left(a\underset{\dot{}}{+}c\right)\underset{\dot{}}{-}a$$
23	22	mpteq2dv	$$⊢x=a\to \left(c\in y⟼\left(x\underset{\dot{}}{+}c\right)\underset{\dot{}}{-}x\right)=\left(c\in y⟼\left(a\underset{\dot{}}{+}c\right)\underset{\dot{}}{-}a\right)$$
24	19 23	syl5eq	$$⊢x=a\to \left(z\in y⟼\left(x\underset{\dot{}}{+}z\right)\underset{\dot{}}{-}x\right)=\left(c\in y⟼\left(a\underset{\dot{}}{+}c\right)\underset{\dot{}}{-}a\right)$$
25	24	rneqd	$$⊢x=a\to \mathrm{ran}\left(z\in y⟼\left(x\underset{\dot{}}{+}z\right)\underset{\dot{}}{-}x\right)=\mathrm{ran}\left(c\in y⟼\left(a\underset{\dot{}}{+}c\right)\underset{\dot{}}{-}a\right)$$
26		mpteq1	$$⊢y=b\to \left(c\in y⟼\left(a\underset{\dot{}}{+}c\right)\underset{\dot{}}{-}a\right)=\left(c\in b⟼\left(a\underset{\dot{}}{+}c\right)\underset{\dot{}}{-}a\right)$$
27	26	rneqd	$$⊢y=b\to \mathrm{ran}\left(c\in y⟼\left(a\underset{\dot{}}{+}c\right)\underset{\dot{}}{-}a\right)=\mathrm{ran}\left(c\in b⟼\left(a\underset{\dot{}}{+}c\right)\underset{\dot{}}{-}a\right)$$
28	25 27	cbvmpov	$$⊢\left(x\in X,y\in \left(P\mathrm{pSyl}G\right)⟼\mathrm{ran}\left(z\in y⟼\left(x\underset{\dot{}}{+}z\right)\underset{\dot{}}{-}x\right)\right)=\left(a\in X,b\in \left(P\mathrm{pSyl}G\right)⟼\mathrm{ran}\left(c\in b⟼\left(a\underset{\dot{}}{+}c\right)\underset{\dot{}}{-}a\right)\right)$$
29	1 2 3 4 5 6 28	sylow3lem1	$$⊢\phi \to \left(x\in X,y\in \left(P\mathrm{pSyl}G\right)⟼\mathrm{ran}\left(z\in y⟼\left(x\underset{\dot{}}{+}z\right)\underset{\dot{}}{-}x\right)\right)\in \left(G\mathrm{GrpAct}\left(P\mathrm{pSyl}G\right)\right)$$
30		eqid	$$⊢G{\upharpoonright }_{𝑠}K=G{\upharpoonright }_{𝑠}K$$
31	30	gasubg	$$⊢\left(\left(x\in X,y\in \left(P\mathrm{pSyl}G\right)⟼\mathrm{ran}\left(z\in y⟼\left(x\underset{\dot{}}{+}z\right)\underset{\dot{}}{-}x\right)\right)\in \left(G\mathrm{GrpAct}\left(P\mathrm{pSyl}G\right)\right)\wedge K\in \mathrm{SubGrp}\left(G\right)\right)\to {\left(x\in X,y\in \left(P\mathrm{pSyl}G\right)⟼\mathrm{ran}\left(z\in y⟼\left(x\underset{\dot{}}{+}z\right)\underset{\dot{}}{-}x\right)\right)\upharpoonright }_{\left(K\times \left(P\mathrm{pSyl}G\right)\right)}\in \left(\left(G{\upharpoonright }_{𝑠}K\right)\mathrm{GrpAct}\left(P\mathrm{pSyl}G\right)\right)$$
32	29 10 31	syl2anc	$$⊢\phi \to {\left(x\in X,y\in \left(P\mathrm{pSyl}G\right)⟼\mathrm{ran}\left(z\in y⟼\left(x\underset{\dot{}}{+}z\right)\underset{\dot{}}{-}x\right)\right)\upharpoonright }_{\left(K\times \left(P\mathrm{pSyl}G\right)\right)}\in \left(\left(G{\upharpoonright }_{𝑠}K\right)\mathrm{GrpAct}\left(P\mathrm{pSyl}G\right)\right)$$
33	16 32	eqeltrrd	$$⊢\phi \to \underset{\dot{}}{\oplus }\in \left(\left(G{\upharpoonright }_{𝑠}K\right)\mathrm{GrpAct}\left(P\mathrm{pSyl}G\right)\right)$$