Theorem sylow3lem4

Description: Lemma for sylow3 , first part. The number of Sylow subgroups is a divisor of the size of G reduced by the size of a Sylow subgroup of G . (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}$$
	sylow3lem1.a	$$⊢\underset{\dot{}}{+}={+}_G$$
	sylow3lem1.d	$$⊢\underset{\dot{}}{-}={-}_G$$
	sylow3lem1.m	$$⊢\underset{\dot{}}{\oplus }=\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)$$
	sylow3lem2.k	$$⊢\phi \to K\in \left(P\mathrm{pSyl}G\right)$$
	sylow3lem2.h	$$⊢H=\left\{u\in X|u\underset{\dot{}}{\oplus }K=K\right\}$$
	sylow3lem2.n	$$⊢N=\left\{x\in X|\forall y\in X\left(x\underset{\dot{}}{+}y\in K\leftrightarrow y\underset{\dot{}}{+}x\in K\right)\right\}$$
Assertion	sylow3lem4	$$⊢\phi \to \left|P\mathrm{pSyl}G\right|\parallel \left(\frac{\left|X\right|}{P^{P\mathrm{pCnt}\left|X\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		sylow3lem1.a	$$⊢\underset{\dot{}}{+}={+}_G$$
6		sylow3lem1.d	$$⊢\underset{\dot{}}{-}={-}_G$$
7		sylow3lem1.m	$$⊢\underset{\dot{}}{\oplus }=\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)$$
8		sylow3lem2.k	$$⊢\phi \to K\in \left(P\mathrm{pSyl}G\right)$$
9		sylow3lem2.h	$$⊢H=\left\{u\in X|u\underset{\dot{}}{\oplus }K=K\right\}$$
10		sylow3lem2.n	$$⊢N=\left\{x\in X|\forall y\in X\left(x\underset{\dot{}}{+}y\in K\leftrightarrow y\underset{\dot{}}{+}x\in K\right)\right\}$$
11	1 2 3 4 5 6 7 8 9 10	sylow3lem3	$$⊢\phi \to \left|P\mathrm{pSyl}G\right|=\left|X/\left(G{~}_{\mathit{QG}}N\right)\right|$$
12		slwsubg	$$⊢K\in \left(P\mathrm{pSyl}G\right)\to K\in \mathrm{SubGrp}\left(G\right)$$
13	8 12	syl	$$⊢\phi \to K\in \mathrm{SubGrp}\left(G\right)$$
14		eqid	$$⊢G{\upharpoonright }_{𝑠}N=G{\upharpoonright }_{𝑠}N$$
15	10 1 5 14	nmznsg	$$⊢K\in \mathrm{SubGrp}\left(G\right)\to K\in \mathrm{NrmSGrp}\left(G{\upharpoonright }_{𝑠}N\right)$$
16		nsgsubg	$$⊢K\in \mathrm{NrmSGrp}\left(G{\upharpoonright }_{𝑠}N\right)\to K\in \mathrm{SubGrp}\left(G{\upharpoonright }_{𝑠}N\right)$$
17	15 16	syl	$$⊢K\in \mathrm{SubGrp}\left(G\right)\to K\in \mathrm{SubGrp}\left(G{\upharpoonright }_{𝑠}N\right)$$
18	13 17	syl	$$⊢\phi \to K\in \mathrm{SubGrp}\left(G{\upharpoonright }_{𝑠}N\right)$$
19	10 1 5	nmzsubg	$$⊢G\in \mathrm{Grp}\to N\in \mathrm{SubGrp}\left(G\right)$$
20	2 19	syl	$$⊢\phi \to N\in \mathrm{SubGrp}\left(G\right)$$
21	14	subgbas	$$⊢N\in \mathrm{SubGrp}\left(G\right)\to N={\mathrm{Base}}_{\left(G{\upharpoonright }_{𝑠}N\right)}$$
22	20 21	syl	$$⊢\phi \to N={\mathrm{Base}}_{\left(G{\upharpoonright }_{𝑠}N\right)}$$
23	1	subgss	$$⊢N\in \mathrm{SubGrp}\left(G\right)\to N\subseteq X$$
24	20 23	syl	$$⊢\phi \to N\subseteq X$$
25	3 24	ssfid	$$⊢\phi \to N\in \mathrm{Fin}$$
26	22 25	eqeltrrd	$$⊢\phi \to {\mathrm{Base}}_{\left(G{\upharpoonright }_{𝑠}N\right)}\in \mathrm{Fin}$$
27		eqid	$$⊢{\mathrm{Base}}_{\left(G{\upharpoonright }_{𝑠}N\right)}={\mathrm{Base}}_{\left(G{\upharpoonright }_{𝑠}N\right)}$$
28	27	lagsubg	$$⊢\left(K\in \mathrm{SubGrp}\left(G{\upharpoonright }_{𝑠}N\right)\wedge {\mathrm{Base}}_{\left(G{\upharpoonright }_{𝑠}N\right)}\in \mathrm{Fin}\right)\to \left|K\right|\parallel \left|{\mathrm{Base}}_{\left(G{\upharpoonright }_{𝑠}N\right)}\right|$$
29	18 26 28	syl2anc	$$⊢\phi \to \left|K\right|\parallel \left|{\mathrm{Base}}_{\left(G{\upharpoonright }_{𝑠}N\right)}\right|$$
30	22	fveq2d	$$⊢\phi \to \left|N\right|=\left|{\mathrm{Base}}_{\left(G{\upharpoonright }_{𝑠}N\right)}\right|$$
31	29 30	breqtrrd	$$⊢\phi \to \left|K\right|\parallel \left|N\right|$$
32		eqid	$$⊢0_G=0_G$$
33	32	subg0cl	$$⊢K\in \mathrm{SubGrp}\left(G\right)\to 0_G\in K$$
34	13 33	syl	$$⊢\phi \to 0_G\in K$$
35	34	ne0d	$$⊢\phi \to K\ne \varnothing$$
36	1	subgss	$$⊢K\in \mathrm{SubGrp}\left(G\right)\to K\subseteq X$$
37	13 36	syl	$$⊢\phi \to K\subseteq X$$
38	3 37	ssfid	$$⊢\phi \to K\in \mathrm{Fin}$$
39		hashnncl	$$⊢K\in \mathrm{Fin}\to \left(\left|K\right|\in \mathbb{N}\leftrightarrow K\ne \varnothing \right)$$
40	38 39	syl	$$⊢\phi \to \left(\left|K\right|\in \mathbb{N}\leftrightarrow K\ne \varnothing \right)$$
41	35 40	mpbird	$$⊢\phi \to \left|K\right|\in \mathbb{N}$$
42	41	nnzd	$$⊢\phi \to \left|K\right|\in \mathbb{Z}$$
43		hashcl	$$⊢N\in \mathrm{Fin}\to \left|N\right|\in {\mathbb{N}}_0$$
44	25 43	syl	$$⊢\phi \to \left|N\right|\in {\mathbb{N}}_0$$
45	44	nn0zd	$$⊢\phi \to \left|N\right|\in \mathbb{Z}$$
46		pwfi	$$⊢X\in \mathrm{Fin}\leftrightarrow 𝒫X\in \mathrm{Fin}$$
47	3 46	sylib	$$⊢\phi \to 𝒫X\in \mathrm{Fin}$$
48		eqid	$$⊢G{~}_{\mathit{QG}}N=G{~}_{\mathit{QG}}N$$
49	1 48	eqger	$$⊢N\in \mathrm{SubGrp}\left(G\right)\to \left(G{~}_{\mathit{QG}}N\right)\mathrm{Er}X$$
50	20 49	syl	$$⊢\phi \to \left(G{~}_{\mathit{QG}}N\right)\mathrm{Er}X$$
51	50	qsss	$$⊢\phi \to X/\left(G{~}_{\mathit{QG}}N\right)\subseteq 𝒫X$$
52	47 51	ssfid	$$⊢\phi \to X/\left(G{~}_{\mathit{QG}}N\right)\in \mathrm{Fin}$$
53		hashcl	$$⊢X/\left(G{~}_{\mathit{QG}}N\right)\in \mathrm{Fin}\to \left|X/\left(G{~}_{\mathit{QG}}N\right)\right|\in {\mathbb{N}}_0$$
54	52 53	syl	$$⊢\phi \to \left|X/\left(G{~}_{\mathit{QG}}N\right)\right|\in {\mathbb{N}}_0$$
55	54	nn0zd	$$⊢\phi \to \left|X/\left(G{~}_{\mathit{QG}}N\right)\right|\in \mathbb{Z}$$
56		dvdscmul	$$⊢\left(\left|K\right|\in \mathbb{Z}\wedge \left|N\right|\in \mathbb{Z}\wedge \left|X/\left(G{~}_{\mathit{QG}}N\right)\right|\in \mathbb{Z}\right)\to \left(\left|K\right|\parallel \left|N\right|\to \left|X/\left(G{~}_{\mathit{QG}}N\right)\right|\left|K\right|\parallel \left|X/\left(G{~}_{\mathit{QG}}N\right)\right|\left|N\right|\right)$$
57	42 45 55 56	syl3anc	$$⊢\phi \to \left(\left|K\right|\parallel \left|N\right|\to \left|X/\left(G{~}_{\mathit{QG}}N\right)\right|\left|K\right|\parallel \left|X/\left(G{~}_{\mathit{QG}}N\right)\right|\left|N\right|\right)$$
58	31 57	mpd	$$⊢\phi \to \left|X/\left(G{~}_{\mathit{QG}}N\right)\right|\left|K\right|\parallel \left|X/\left(G{~}_{\mathit{QG}}N\right)\right|\left|N\right|$$
59		hashcl	$$⊢X\in \mathrm{Fin}\to \left|X\right|\in {\mathbb{N}}_0$$
60	3 59	syl	$$⊢\phi \to \left|X\right|\in {\mathbb{N}}_0$$
61	60	nn0cnd	$$⊢\phi \to \left|X\right|\in ℂ$$
62	41	nncnd	$$⊢\phi \to \left|K\right|\in ℂ$$
63	41	nnne0d	$$⊢\phi \to \left|K\right|\ne 0$$
64	61 62 63	divcan1d	$$⊢\phi \to \left(\frac{\left|X\right|}{\left|K\right|}\right)\left|K\right|=\left|X\right|$$
65	1 48 20 3	lagsubg2	$$⊢\phi \to \left|X\right|=\left|X/\left(G{~}_{\mathit{QG}}N\right)\right|\left|N\right|$$
66	64 65	eqtrd	$$⊢\phi \to \left(\frac{\left|X\right|}{\left|K\right|}\right)\left|K\right|=\left|X/\left(G{~}_{\mathit{QG}}N\right)\right|\left|N\right|$$
67	58 66	breqtrrd	$$⊢\phi \to \left|X/\left(G{~}_{\mathit{QG}}N\right)\right|\left|K\right|\parallel \left(\frac{\left|X\right|}{\left|K\right|}\right)\left|K\right|$$
68	1	lagsubg	$$⊢\left(K\in \mathrm{SubGrp}\left(G\right)\wedge X\in \mathrm{Fin}\right)\to \left|K\right|\parallel \left|X\right|$$
69	13 3 68	syl2anc	$$⊢\phi \to \left|K\right|\parallel \left|X\right|$$
70	60	nn0zd	$$⊢\phi \to \left|X\right|\in \mathbb{Z}$$
71		dvdsval2	$$⊢\left(\left|K\right|\in \mathbb{Z}\wedge \left|K\right|\ne 0\wedge \left|X\right|\in \mathbb{Z}\right)\to \left(\left|K\right|\parallel \left|X\right|\leftrightarrow \frac{\left|X\right|}{\left|K\right|}\in \mathbb{Z}\right)$$
72	42 63 70 71	syl3anc	$$⊢\phi \to \left(\left|K\right|\parallel \left|X\right|\leftrightarrow \frac{\left|X\right|}{\left|K\right|}\in \mathbb{Z}\right)$$
73	69 72	mpbid	$$⊢\phi \to \frac{\left|X\right|}{\left|K\right|}\in \mathbb{Z}$$
74		dvdsmulcr	$$⊢\left(\left|X/\left(G{~}_{\mathit{QG}}N\right)\right|\in \mathbb{Z}\wedge \frac{\left|X\right|}{\left|K\right|}\in \mathbb{Z}\wedge \left(\left|K\right|\in \mathbb{Z}\wedge \left|K\right|\ne 0\right)\right)\to \left(\left|X/\left(G{~}_{\mathit{QG}}N\right)\right|\left|K\right|\parallel \left(\frac{\left|X\right|}{\left|K\right|}\right)\left|K\right|\leftrightarrow \left|X/\left(G{~}_{\mathit{QG}}N\right)\right|\parallel \left(\frac{\left|X\right|}{\left|K\right|}\right)\right)$$
75	55 73 42 63 74	syl112anc	$$⊢\phi \to \left(\left|X/\left(G{~}_{\mathit{QG}}N\right)\right|\left|K\right|\parallel \left(\frac{\left|X\right|}{\left|K\right|}\right)\left|K\right|\leftrightarrow \left|X/\left(G{~}_{\mathit{QG}}N\right)\right|\parallel \left(\frac{\left|X\right|}{\left|K\right|}\right)\right)$$
76	67 75	mpbid	$$⊢\phi \to \left|X/\left(G{~}_{\mathit{QG}}N\right)\right|\parallel \left(\frac{\left|X\right|}{\left|K\right|}\right)$$
77	1 3 8	slwhash	$$⊢\phi \to \left|K\right|=P^{P\mathrm{pCnt}\left|X\right|}$$
78	77	oveq2d	$$⊢\phi \to \frac{\left|X\right|}{\left|K\right|}=\frac{\left|X\right|}{P^{P\mathrm{pCnt}\left|X\right|}}$$
79	76 78	breqtrd	$$⊢\phi \to \left|X/\left(G{~}_{\mathit{QG}}N\right)\right|\parallel \left(\frac{\left|X\right|}{P^{P\mathrm{pCnt}\left|X\right|}}\right)$$
80	11 79	eqbrtrd	$$⊢\phi \to \left|P\mathrm{pSyl}G\right|\parallel \left(\frac{\left|X\right|}{P^{P\mathrm{pCnt}\left|X\right|}}\right)$$