Theorem sylow1lem5

Description: Lemma for sylow1 . Using Lagrange's theorem and the orbit-stabilizer theorem, show that there is a subgroup with size exactly P ^ N . (Contributed by Mario Carneiro, 16-Jan-2015)

	Ref	Expression
Hypotheses	sylow1.x	$$⊢X={\mathrm{Base}}_G$$
	sylow1.g	$$⊢\phi \to G\in \mathrm{Grp}$$
	sylow1.f	$$⊢\phi \to X\in \mathrm{Fin}$$
	sylow1.p	$$⊢\phi \to P\in \mathbb{P}$$
	sylow1.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	sylow1.d	$$⊢\phi \to P^N\parallel \left|X\right|$$
	sylow1lem.a	$$⊢\underset{\dot{}}{+}={+}_G$$
	sylow1lem.s	$$⊢S=\left\{s\in 𝒫X|\left|s\right|=P^N\right\}$$
	sylow1lem.m	$$⊢\underset{\dot{}}{\oplus }=\left(x\in X,y\in S⟼\mathrm{ran}\left(z\in y⟼x\underset{\dot{}}{+}z\right)\right)$$
	sylow1lem3.1	$$⊢\underset{\dot{}}{\sim }=\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq S\wedge \exists g\in Xg\underset{\dot{}}{\oplus }x=y\right)\right\}$$
	sylow1lem4.b	$$⊢\phi \to B\in S$$
	sylow1lem4.h	$$⊢H=\left\{u\in X|u\underset{\dot{}}{\oplus }B=B\right\}$$
	sylow1lem5.l	$$⊢\phi \to P\mathrm{pCnt}\left|\left[B\right]\underset{\dot{}}{\sim }\right|\le \left(P\mathrm{pCnt}\left|X\right|\right)-N$$
Assertion	sylow1lem5	$$⊢\phi \to \exists h\in \mathrm{SubGrp}\left(G\right)\left|h\right|=P^N$$

Proof

Step	Hyp	Ref	Expression
1		sylow1.x	$$⊢X={\mathrm{Base}}_G$$
2		sylow1.g	$$⊢\phi \to G\in \mathrm{Grp}$$
3		sylow1.f	$$⊢\phi \to X\in \mathrm{Fin}$$
4		sylow1.p	$$⊢\phi \to P\in \mathbb{P}$$
5		sylow1.n	$$⊢\phi \to N\in {\mathbb{N}}_0$$
6		sylow1.d	$$⊢\phi \to P^N\parallel \left|X\right|$$
7		sylow1lem.a	$$⊢\underset{\dot{}}{+}={+}_G$$
8		sylow1lem.s	$$⊢S=\left\{s\in 𝒫X|\left|s\right|=P^N\right\}$$
9		sylow1lem.m	$$⊢\underset{\dot{}}{\oplus }=\left(x\in X,y\in S⟼\mathrm{ran}\left(z\in y⟼x\underset{\dot{}}{+}z\right)\right)$$
10		sylow1lem3.1	$$⊢\underset{\dot{}}{\sim }=\left\{⟨x,y⟩|\left(\left\{x,y\right\}\subseteq S\wedge \exists g\in Xg\underset{\dot{}}{\oplus }x=y\right)\right\}$$
11		sylow1lem4.b	$$⊢\phi \to B\in S$$
12		sylow1lem4.h	$$⊢H=\left\{u\in X|u\underset{\dot{}}{\oplus }B=B\right\}$$
13		sylow1lem5.l	$$⊢\phi \to P\mathrm{pCnt}\left|\left[B\right]\underset{\dot{}}{\sim }\right|\le \left(P\mathrm{pCnt}\left|X\right|\right)-N$$
14	1 2 3 4 5 6 7 8 9	sylow1lem2	$$⊢\phi \to \underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}S\right)$$
15	1 12	gastacl	$$⊢\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}S\right)\wedge B\in S\right)\to H\in \mathrm{SubGrp}\left(G\right)$$
16	14 11 15	syl2anc	$$⊢\phi \to H\in \mathrm{SubGrp}\left(G\right)$$
17	1 2 3 4 5 6 7 8 9 10 11 12	sylow1lem4	$$⊢\phi \to \left|H\right|\le P^N$$
18	10 1	gaorber	$$⊢\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}S\right)\to \underset{\dot{}}{\sim }\mathrm{Er}S$$
19	14 18	syl	$$⊢\phi \to \underset{\dot{}}{\sim }\mathrm{Er}S$$
20		erdm	$$⊢\underset{\dot{}}{\sim }\mathrm{Er}S\to \mathrm{dom}\underset{\dot{}}{\sim }=S$$
21	19 20	syl	$$⊢\phi \to \mathrm{dom}\underset{\dot{}}{\sim }=S$$
22	11 21	eleqtrrd	$$⊢\phi \to B\in \mathrm{dom}\underset{\dot{}}{\sim }$$
23		ecdmn0	$$⊢B\in \mathrm{dom}\underset{\dot{}}{\sim }\leftrightarrow \left[B\right]\underset{\dot{}}{\sim }\ne \varnothing$$
24	22 23	sylib	$$⊢\phi \to \left[B\right]\underset{\dot{}}{\sim }\ne \varnothing$$
25		pwfi	$$⊢X\in \mathrm{Fin}\leftrightarrow 𝒫X\in \mathrm{Fin}$$
26	3 25	sylib	$$⊢\phi \to 𝒫X\in \mathrm{Fin}$$
27	8	ssrab3	$$⊢S\subseteq 𝒫X$$
28		ssfi	$$⊢\left(𝒫X\in \mathrm{Fin}\wedge S\subseteq 𝒫X\right)\to S\in \mathrm{Fin}$$
29	26 27 28	sylancl	$$⊢\phi \to S\in \mathrm{Fin}$$
30	19	ecss	$$⊢\phi \to \left[B\right]\underset{\dot{}}{\sim }\subseteq S$$
31	29 30	ssfid	$$⊢\phi \to \left[B\right]\underset{\dot{}}{\sim }\in \mathrm{Fin}$$
32		hashnncl	$$⊢\left[B\right]\underset{\dot{}}{\sim }\in \mathrm{Fin}\to \left(\left|\left[B\right]\underset{\dot{}}{\sim }\right|\in \mathbb{N}\leftrightarrow \left[B\right]\underset{\dot{}}{\sim }\ne \varnothing \right)$$
33	31 32	syl	$$⊢\phi \to \left(\left|\left[B\right]\underset{\dot{}}{\sim }\right|\in \mathbb{N}\leftrightarrow \left[B\right]\underset{\dot{}}{\sim }\ne \varnothing \right)$$
34	24 33	mpbird	$$⊢\phi \to \left|\left[B\right]\underset{\dot{}}{\sim }\right|\in \mathbb{N}$$
35	4 34	pccld	$$⊢\phi \to P\mathrm{pCnt}\left|\left[B\right]\underset{\dot{}}{\sim }\right|\in {\mathbb{N}}_0$$
36	35	nn0red	$$⊢\phi \to P\mathrm{pCnt}\left|\left[B\right]\underset{\dot{}}{\sim }\right|\in ℝ$$
37	5	nn0red	$$⊢\phi \to N\in ℝ$$
38	1	grpbn0	$$⊢G\in \mathrm{Grp}\to X\ne \varnothing$$
39	2 38	syl	$$⊢\phi \to X\ne \varnothing$$
40		hashnncl	$$⊢X\in \mathrm{Fin}\to \left(\left|X\right|\in \mathbb{N}\leftrightarrow X\ne \varnothing \right)$$
41	3 40	syl	$$⊢\phi \to \left(\left|X\right|\in \mathbb{N}\leftrightarrow X\ne \varnothing \right)$$
42	39 41	mpbird	$$⊢\phi \to \left|X\right|\in \mathbb{N}$$
43	4 42	pccld	$$⊢\phi \to P\mathrm{pCnt}\left|X\right|\in {\mathbb{N}}_0$$
44	43	nn0red	$$⊢\phi \to P\mathrm{pCnt}\left|X\right|\in ℝ$$
45		leaddsub	$$⊢\left(P\mathrm{pCnt}\left|\left[B\right]\underset{\dot{}}{\sim }\right|\in ℝ\wedge N\in ℝ\wedge P\mathrm{pCnt}\left|X\right|\in ℝ\right)\to \left(\left(P\mathrm{pCnt}\left|\left[B\right]\underset{\dot{}}{\sim }\right|\right)+N\le P\mathrm{pCnt}\left|X\right|\leftrightarrow P\mathrm{pCnt}\left|\left[B\right]\underset{\dot{}}{\sim }\right|\le \left(P\mathrm{pCnt}\left|X\right|\right)-N\right)$$
46	36 37 44 45	syl3anc	$$⊢\phi \to \left(\left(P\mathrm{pCnt}\left|\left[B\right]\underset{\dot{}}{\sim }\right|\right)+N\le P\mathrm{pCnt}\left|X\right|\leftrightarrow P\mathrm{pCnt}\left|\left[B\right]\underset{\dot{}}{\sim }\right|\le \left(P\mathrm{pCnt}\left|X\right|\right)-N\right)$$
47	13 46	mpbird	$$⊢\phi \to \left(P\mathrm{pCnt}\left|\left[B\right]\underset{\dot{}}{\sim }\right|\right)+N\le P\mathrm{pCnt}\left|X\right|$$
48		eqid	$$⊢G{~}_{\mathit{QG}}H=G{~}_{\mathit{QG}}H$$
49	1 12 48 10	orbsta2	$$⊢\left(\left(\underset{\dot{}}{\oplus }\in \left(G\mathrm{GrpAct}S\right)\wedge B\in S\right)\wedge X\in \mathrm{Fin}\right)\to \left|X\right|=\left|\left[B\right]\underset{\dot{}}{\sim }\right|\left|H\right|$$
50	14 11 3 49	syl21anc	$$⊢\phi \to \left|X\right|=\left|\left[B\right]\underset{\dot{}}{\sim }\right|\left|H\right|$$
51	50	oveq2d	$$⊢\phi \to P\mathrm{pCnt}\left|X\right|=P\mathrm{pCnt}\left|\left[B\right]\underset{\dot{}}{\sim }\right|\left|H\right|$$
52	34	nnzd	$$⊢\phi \to \left|\left[B\right]\underset{\dot{}}{\sim }\right|\in \mathbb{Z}$$
53	34	nnne0d	$$⊢\phi \to \left|\left[B\right]\underset{\dot{}}{\sim }\right|\ne 0$$
54		eqid	$$⊢0_G=0_G$$
55	54	subg0cl	$$⊢H\in \mathrm{SubGrp}\left(G\right)\to 0_G\in H$$
56	16 55	syl	$$⊢\phi \to 0_G\in H$$
57	56	ne0d	$$⊢\phi \to H\ne \varnothing$$
58	12	ssrab3	$$⊢H\subseteq X$$
59		ssfi	$$⊢\left(X\in \mathrm{Fin}\wedge H\subseteq X\right)\to H\in \mathrm{Fin}$$
60	3 58 59	sylancl	$$⊢\phi \to H\in \mathrm{Fin}$$
61		hashnncl	$$⊢H\in \mathrm{Fin}\to \left(\left|H\right|\in \mathbb{N}\leftrightarrow H\ne \varnothing \right)$$
62	60 61	syl	$$⊢\phi \to \left(\left|H\right|\in \mathbb{N}\leftrightarrow H\ne \varnothing \right)$$
63	57 62	mpbird	$$⊢\phi \to \left|H\right|\in \mathbb{N}$$
64	63	nnzd	$$⊢\phi \to \left|H\right|\in \mathbb{Z}$$
65	63	nnne0d	$$⊢\phi \to \left|H\right|\ne 0$$
66		pcmul	$$⊢\left(P\in \mathbb{P}\wedge \left(\left|\left[B\right]\underset{\dot{}}{\sim }\right|\in \mathbb{Z}\wedge \left|\left[B\right]\underset{\dot{}}{\sim }\right|\ne 0\right)\wedge \left(\left|H\right|\in \mathbb{Z}\wedge \left|H\right|\ne 0\right)\right)\to P\mathrm{pCnt}\left|\left[B\right]\underset{\dot{}}{\sim }\right|\left|H\right|=\left(P\mathrm{pCnt}\left|\left[B\right]\underset{\dot{}}{\sim }\right|\right)+\left(P\mathrm{pCnt}\left|H\right|\right)$$
67	4 52 53 64 65 66	syl122anc	$$⊢\phi \to P\mathrm{pCnt}\left|\left[B\right]\underset{\dot{}}{\sim }\right|\left|H\right|=\left(P\mathrm{pCnt}\left|\left[B\right]\underset{\dot{}}{\sim }\right|\right)+\left(P\mathrm{pCnt}\left|H\right|\right)$$
68	51 67	eqtrd	$$⊢\phi \to P\mathrm{pCnt}\left|X\right|=\left(P\mathrm{pCnt}\left|\left[B\right]\underset{\dot{}}{\sim }\right|\right)+\left(P\mathrm{pCnt}\left|H\right|\right)$$
69	47 68	breqtrd	$$⊢\phi \to \left(P\mathrm{pCnt}\left|\left[B\right]\underset{\dot{}}{\sim }\right|\right)+N\le \left(P\mathrm{pCnt}\left|\left[B\right]\underset{\dot{}}{\sim }\right|\right)+\left(P\mathrm{pCnt}\left|H\right|\right)$$
70	4 63	pccld	$$⊢\phi \to P\mathrm{pCnt}\left|H\right|\in {\mathbb{N}}_0$$
71	70	nn0red	$$⊢\phi \to P\mathrm{pCnt}\left|H\right|\in ℝ$$
72	37 71 36	leadd2d	$$⊢\phi \to \left(N\le P\mathrm{pCnt}\left|H\right|\leftrightarrow \left(P\mathrm{pCnt}\left|\left[B\right]\underset{\dot{}}{\sim }\right|\right)+N\le \left(P\mathrm{pCnt}\left|\left[B\right]\underset{\dot{}}{\sim }\right|\right)+\left(P\mathrm{pCnt}\left|H\right|\right)\right)$$
73	69 72	mpbird	$$⊢\phi \to N\le P\mathrm{pCnt}\left|H\right|$$
74		pcdvdsb	$$⊢\left(P\in \mathbb{P}\wedge \left|H\right|\in \mathbb{Z}\wedge N\in {\mathbb{N}}_0\right)\to \left(N\le P\mathrm{pCnt}\left|H\right|\leftrightarrow P^N\parallel \left|H\right|\right)$$
75	4 64 5 74	syl3anc	$$⊢\phi \to \left(N\le P\mathrm{pCnt}\left|H\right|\leftrightarrow P^N\parallel \left|H\right|\right)$$
76	73 75	mpbid	$$⊢\phi \to P^N\parallel \left|H\right|$$
77		prmnn	$$⊢P\in \mathbb{P}\to P\in \mathbb{N}$$
78	4 77	syl	$$⊢\phi \to P\in \mathbb{N}$$
79	78 5	nnexpcld	$$⊢\phi \to P^N\in \mathbb{N}$$
80	79	nnzd	$$⊢\phi \to P^N\in \mathbb{Z}$$
81		dvdsle	$$⊢\left(P^N\in \mathbb{Z}\wedge \left|H\right|\in \mathbb{N}\right)\to \left(P^N\parallel \left|H\right|\to P^N\le \left|H\right|\right)$$
82	80 63 81	syl2anc	$$⊢\phi \to \left(P^N\parallel \left|H\right|\to P^N\le \left|H\right|\right)$$
83	76 82	mpd	$$⊢\phi \to P^N\le \left|H\right|$$
84		hashcl	$$⊢H\in \mathrm{Fin}\to \left|H\right|\in {\mathbb{N}}_0$$
85	60 84	syl	$$⊢\phi \to \left|H\right|\in {\mathbb{N}}_0$$
86	85	nn0red	$$⊢\phi \to \left|H\right|\in ℝ$$
87	79	nnred	$$⊢\phi \to P^N\in ℝ$$
88	86 87	letri3d	$$⊢\phi \to \left(\left|H\right|=P^N\leftrightarrow \left(\left|H\right|\le P^N\wedge P^N\le \left|H\right|\right)\right)$$
89	17 83 88	mpbir2and	$$⊢\phi \to \left|H\right|=P^N$$
90		fveqeq2	$$⊢h=H\to \left(\left|h\right|=P^N\leftrightarrow \left|H\right|=P^N\right)$$
91	90	rspcev	$$⊢\left(H\in \mathrm{SubGrp}\left(G\right)\wedge \left|H\right|=P^N\right)\to \exists h\in \mathrm{SubGrp}\left(G\right)\left|h\right|=P^N$$
92	16 89 91	syl2anc	$$⊢\phi \to \exists h\in \mathrm{SubGrp}\left(G\right)\left|h\right|=P^N$$