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	⊢ 𝑋 = ( Base ‘ 𝐺 )
	sylow1.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
	sylow1.f	⊢ ( 𝜑 → 𝑋 ∈ Fin )
	sylow1.p	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
	sylow1.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
	sylow1.d	⊢ ( 𝜑 → ( 𝑃 ↑ 𝑁 ) ∥ ( ♯ ‘ 𝑋 ) )
	sylow1lem.a	⊢ + = ( +g ‘ 𝐺 )
	sylow1lem.s	⊢ 𝑆 = { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) }
	sylow1lem.m	⊢ ⊕ = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑆 ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) )
	sylow1lem3.1	⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑆 ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) }
	sylow1lem4.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
	sylow1lem4.h	⊢ 𝐻 = { 𝑢 ∈ 𝑋 ∣ ( 𝑢 ⊕ 𝐵 ) = 𝐵 }
	sylow1lem5.l	⊢ ( 𝜑 → ( 𝑃 pCnt ( ♯ ‘ [ 𝐵 ] ∼ ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) )
Assertion	sylow1lem5	⊢ ( 𝜑 → ∃ ℎ ∈ ( SubGrp ‘ 𝐺 ) ( ♯ ‘ ℎ ) = ( 𝑃 ↑ 𝑁 ) )

Proof

Step	Hyp	Ref	Expression
1		sylow1.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		sylow1.g	⊢ ( 𝜑 → 𝐺 ∈ Grp )
3		sylow1.f	⊢ ( 𝜑 → 𝑋 ∈ Fin )
4		sylow1.p	⊢ ( 𝜑 → 𝑃 ∈ ℙ )
5		sylow1.n	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
6		sylow1.d	⊢ ( 𝜑 → ( 𝑃 ↑ 𝑁 ) ∥ ( ♯ ‘ 𝑋 ) )
7		sylow1lem.a	⊢ + = ( +g ‘ 𝐺 )
8		sylow1lem.s	⊢ 𝑆 = { 𝑠 ∈ 𝒫 𝑋 ∣ ( ♯ ‘ 𝑠 ) = ( 𝑃 ↑ 𝑁 ) }
9		sylow1lem.m	⊢ ⊕ = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑆 ↦ ran ( 𝑧 ∈ 𝑦 ↦ ( 𝑥 + 𝑧 ) ) )
10		sylow1lem3.1	⊢ ∼ = { ⟨ 𝑥 , 𝑦 ⟩ ∣ ( { 𝑥 , 𝑦 } ⊆ 𝑆 ∧ ∃ 𝑔 ∈ 𝑋 ( 𝑔 ⊕ 𝑥 ) = 𝑦 ) }
11		sylow1lem4.b	⊢ ( 𝜑 → 𝐵 ∈ 𝑆 )
12		sylow1lem4.h	⊢ 𝐻 = { 𝑢 ∈ 𝑋 ∣ ( 𝑢 ⊕ 𝐵 ) = 𝐵 }
13		sylow1lem5.l	⊢ ( 𝜑 → ( 𝑃 pCnt ( ♯ ‘ [ 𝐵 ] ∼ ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) )
14	1 2 3 4 5 6 7 8 9	sylow1lem2	⊢ ( 𝜑 → ⊕ ∈ ( 𝐺 GrpAct 𝑆 ) )
15	1 12	gastacl	⊢ ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑆 ) ∧ 𝐵 ∈ 𝑆 ) → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) )
16	14 11 15	syl2anc	⊢ ( 𝜑 → 𝐻 ∈ ( SubGrp ‘ 𝐺 ) )
17	1 2 3 4 5 6 7 8 9 10 11 12	sylow1lem4	⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) ≤ ( 𝑃 ↑ 𝑁 ) )
18	10 1	gaorber	⊢ ( ⊕ ∈ ( 𝐺 GrpAct 𝑆 ) → ∼ Er 𝑆 )
19	14 18	syl	⊢ ( 𝜑 → ∼ Er 𝑆 )
20		erdm	⊢ ( ∼ Er 𝑆 → dom ∼ = 𝑆 )
21	19 20	syl	⊢ ( 𝜑 → dom ∼ = 𝑆 )
22	11 21	eleqtrrd	⊢ ( 𝜑 → 𝐵 ∈ dom ∼ )
23		ecdmn0	⊢ ( 𝐵 ∈ dom ∼ ↔ [ 𝐵 ] ∼ ≠ ∅ )
24	22 23	sylib	⊢ ( 𝜑 → [ 𝐵 ] ∼ ≠ ∅ )
25		pwfi	⊢ ( 𝑋 ∈ Fin ↔ 𝒫 𝑋 ∈ Fin )
26	3 25	sylib	⊢ ( 𝜑 → 𝒫 𝑋 ∈ Fin )
27	8	ssrab3	⊢ 𝑆 ⊆ 𝒫 𝑋
28		ssfi	⊢ ( ( 𝒫 𝑋 ∈ Fin ∧ 𝑆 ⊆ 𝒫 𝑋 ) → 𝑆 ∈ Fin )
29	26 27 28	sylancl	⊢ ( 𝜑 → 𝑆 ∈ Fin )
30	19	ecss	⊢ ( 𝜑 → [ 𝐵 ] ∼ ⊆ 𝑆 )
31	29 30	ssfid	⊢ ( 𝜑 → [ 𝐵 ] ∼ ∈ Fin )
32		hashnncl	⊢ ( [ 𝐵 ] ∼ ∈ Fin → ( ( ♯ ‘ [ 𝐵 ] ∼ ) ∈ ℕ ↔ [ 𝐵 ] ∼ ≠ ∅ ) )
33	31 32	syl	⊢ ( 𝜑 → ( ( ♯ ‘ [ 𝐵 ] ∼ ) ∈ ℕ ↔ [ 𝐵 ] ∼ ≠ ∅ ) )
34	24 33	mpbird	⊢ ( 𝜑 → ( ♯ ‘ [ 𝐵 ] ∼ ) ∈ ℕ )
35	4 34	pccld	⊢ ( 𝜑 → ( 𝑃 pCnt ( ♯ ‘ [ 𝐵 ] ∼ ) ) ∈ ℕ0 )
36	35	nn0red	⊢ ( 𝜑 → ( 𝑃 pCnt ( ♯ ‘ [ 𝐵 ] ∼ ) ) ∈ ℝ )
37	5	nn0red	⊢ ( 𝜑 → 𝑁 ∈ ℝ )
38	1	grpbn0	⊢ ( 𝐺 ∈ Grp → 𝑋 ≠ ∅ )
39	2 38	syl	⊢ ( 𝜑 → 𝑋 ≠ ∅ )
40		hashnncl	⊢ ( 𝑋 ∈ Fin → ( ( ♯ ‘ 𝑋 ) ∈ ℕ ↔ 𝑋 ≠ ∅ ) )
41	3 40	syl	⊢ ( 𝜑 → ( ( ♯ ‘ 𝑋 ) ∈ ℕ ↔ 𝑋 ≠ ∅ ) )
42	39 41	mpbird	⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) ∈ ℕ )
43	4 42	pccld	⊢ ( 𝜑 → ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ∈ ℕ0 )
44	43	nn0red	⊢ ( 𝜑 → ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ∈ ℝ )
45		leaddsub	⊢ ( ( ( 𝑃 pCnt ( ♯ ‘ [ 𝐵 ] ∼ ) ) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ∈ ℝ ) → ( ( ( 𝑃 pCnt ( ♯ ‘ [ 𝐵 ] ∼ ) ) + 𝑁 ) ≤ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ↔ ( 𝑃 pCnt ( ♯ ‘ [ 𝐵 ] ∼ ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) )
46	36 37 44 45	syl3anc	⊢ ( 𝜑 → ( ( ( 𝑃 pCnt ( ♯ ‘ [ 𝐵 ] ∼ ) ) + 𝑁 ) ≤ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) ↔ ( 𝑃 pCnt ( ♯ ‘ [ 𝐵 ] ∼ ) ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) − 𝑁 ) ) )
47	13 46	mpbird	⊢ ( 𝜑 → ( ( 𝑃 pCnt ( ♯ ‘ [ 𝐵 ] ∼ ) ) + 𝑁 ) ≤ ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) )
48		eqid	⊢ ( 𝐺 ~QG 𝐻 ) = ( 𝐺 ~QG 𝐻 )
49	1 12 48 10	orbsta2	⊢ ( ( ( ⊕ ∈ ( 𝐺 GrpAct 𝑆 ) ∧ 𝐵 ∈ 𝑆 ) ∧ 𝑋 ∈ Fin ) → ( ♯ ‘ 𝑋 ) = ( ( ♯ ‘ [ 𝐵 ] ∼ ) · ( ♯ ‘ 𝐻 ) ) )
50	14 11 3 49	syl21anc	⊢ ( 𝜑 → ( ♯ ‘ 𝑋 ) = ( ( ♯ ‘ [ 𝐵 ] ∼ ) · ( ♯ ‘ 𝐻 ) ) )
51	50	oveq2d	⊢ ( 𝜑 → ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) = ( 𝑃 pCnt ( ( ♯ ‘ [ 𝐵 ] ∼ ) · ( ♯ ‘ 𝐻 ) ) ) )
52	34	nnzd	⊢ ( 𝜑 → ( ♯ ‘ [ 𝐵 ] ∼ ) ∈ ℤ )
53	34	nnne0d	⊢ ( 𝜑 → ( ♯ ‘ [ 𝐵 ] ∼ ) ≠ 0 )
54		eqid	⊢ ( 0g ‘ 𝐺 ) = ( 0g ‘ 𝐺 )
55	54	subg0cl	⊢ ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) → ( 0g ‘ 𝐺 ) ∈ 𝐻 )
56	16 55	syl	⊢ ( 𝜑 → ( 0g ‘ 𝐺 ) ∈ 𝐻 )
57	56	ne0d	⊢ ( 𝜑 → 𝐻 ≠ ∅ )
58	12	ssrab3	⊢ 𝐻 ⊆ 𝑋
59		ssfi	⊢ ( ( 𝑋 ∈ Fin ∧ 𝐻 ⊆ 𝑋 ) → 𝐻 ∈ Fin )
60	3 58 59	sylancl	⊢ ( 𝜑 → 𝐻 ∈ Fin )
61		hashnncl	⊢ ( 𝐻 ∈ Fin → ( ( ♯ ‘ 𝐻 ) ∈ ℕ ↔ 𝐻 ≠ ∅ ) )
62	60 61	syl	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐻 ) ∈ ℕ ↔ 𝐻 ≠ ∅ ) )
63	57 62	mpbird	⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) ∈ ℕ )
64	63	nnzd	⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) ∈ ℤ )
65	63	nnne0d	⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) ≠ 0 )
66		pcmul	⊢ ( ( 𝑃 ∈ ℙ ∧ ( ( ♯ ‘ [ 𝐵 ] ∼ ) ∈ ℤ ∧ ( ♯ ‘ [ 𝐵 ] ∼ ) ≠ 0 ) ∧ ( ( ♯ ‘ 𝐻 ) ∈ ℤ ∧ ( ♯ ‘ 𝐻 ) ≠ 0 ) ) → ( 𝑃 pCnt ( ( ♯ ‘ [ 𝐵 ] ∼ ) · ( ♯ ‘ 𝐻 ) ) ) = ( ( 𝑃 pCnt ( ♯ ‘ [ 𝐵 ] ∼ ) ) + ( 𝑃 pCnt ( ♯ ‘ 𝐻 ) ) ) )
67	4 52 53 64 65 66	syl122anc	⊢ ( 𝜑 → ( 𝑃 pCnt ( ( ♯ ‘ [ 𝐵 ] ∼ ) · ( ♯ ‘ 𝐻 ) ) ) = ( ( 𝑃 pCnt ( ♯ ‘ [ 𝐵 ] ∼ ) ) + ( 𝑃 pCnt ( ♯ ‘ 𝐻 ) ) ) )
68	51 67	eqtrd	⊢ ( 𝜑 → ( 𝑃 pCnt ( ♯ ‘ 𝑋 ) ) = ( ( 𝑃 pCnt ( ♯ ‘ [ 𝐵 ] ∼ ) ) + ( 𝑃 pCnt ( ♯ ‘ 𝐻 ) ) ) )
69	47 68	breqtrd	⊢ ( 𝜑 → ( ( 𝑃 pCnt ( ♯ ‘ [ 𝐵 ] ∼ ) ) + 𝑁 ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ [ 𝐵 ] ∼ ) ) + ( 𝑃 pCnt ( ♯ ‘ 𝐻 ) ) ) )
70	4 63	pccld	⊢ ( 𝜑 → ( 𝑃 pCnt ( ♯ ‘ 𝐻 ) ) ∈ ℕ0 )
71	70	nn0red	⊢ ( 𝜑 → ( 𝑃 pCnt ( ♯ ‘ 𝐻 ) ) ∈ ℝ )
72	37 71 36	leadd2d	⊢ ( 𝜑 → ( 𝑁 ≤ ( 𝑃 pCnt ( ♯ ‘ 𝐻 ) ) ↔ ( ( 𝑃 pCnt ( ♯ ‘ [ 𝐵 ] ∼ ) ) + 𝑁 ) ≤ ( ( 𝑃 pCnt ( ♯ ‘ [ 𝐵 ] ∼ ) ) + ( 𝑃 pCnt ( ♯ ‘ 𝐻 ) ) ) ) )
73	69 72	mpbird	⊢ ( 𝜑 → 𝑁 ≤ ( 𝑃 pCnt ( ♯ ‘ 𝐻 ) ) )
74		pcdvdsb	⊢ ( ( 𝑃 ∈ ℙ ∧ ( ♯ ‘ 𝐻 ) ∈ ℤ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑁 ≤ ( 𝑃 pCnt ( ♯ ‘ 𝐻 ) ) ↔ ( 𝑃 ↑ 𝑁 ) ∥ ( ♯ ‘ 𝐻 ) ) )
75	4 64 5 74	syl3anc	⊢ ( 𝜑 → ( 𝑁 ≤ ( 𝑃 pCnt ( ♯ ‘ 𝐻 ) ) ↔ ( 𝑃 ↑ 𝑁 ) ∥ ( ♯ ‘ 𝐻 ) ) )
76	73 75	mpbid	⊢ ( 𝜑 → ( 𝑃 ↑ 𝑁 ) ∥ ( ♯ ‘ 𝐻 ) )
77		prmnn	⊢ ( 𝑃 ∈ ℙ → 𝑃 ∈ ℕ )
78	4 77	syl	⊢ ( 𝜑 → 𝑃 ∈ ℕ )
79	78 5	nnexpcld	⊢ ( 𝜑 → ( 𝑃 ↑ 𝑁 ) ∈ ℕ )
80	79	nnzd	⊢ ( 𝜑 → ( 𝑃 ↑ 𝑁 ) ∈ ℤ )
81		dvdsle	⊢ ( ( ( 𝑃 ↑ 𝑁 ) ∈ ℤ ∧ ( ♯ ‘ 𝐻 ) ∈ ℕ ) → ( ( 𝑃 ↑ 𝑁 ) ∥ ( ♯ ‘ 𝐻 ) → ( 𝑃 ↑ 𝑁 ) ≤ ( ♯ ‘ 𝐻 ) ) )
82	80 63 81	syl2anc	⊢ ( 𝜑 → ( ( 𝑃 ↑ 𝑁 ) ∥ ( ♯ ‘ 𝐻 ) → ( 𝑃 ↑ 𝑁 ) ≤ ( ♯ ‘ 𝐻 ) ) )
83	76 82	mpd	⊢ ( 𝜑 → ( 𝑃 ↑ 𝑁 ) ≤ ( ♯ ‘ 𝐻 ) )
84		hashcl	⊢ ( 𝐻 ∈ Fin → ( ♯ ‘ 𝐻 ) ∈ ℕ0 )
85	60 84	syl	⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) ∈ ℕ0 )
86	85	nn0red	⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) ∈ ℝ )
87	79	nnred	⊢ ( 𝜑 → ( 𝑃 ↑ 𝑁 ) ∈ ℝ )
88	86 87	letri3d	⊢ ( 𝜑 → ( ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ 𝑁 ) ↔ ( ( ♯ ‘ 𝐻 ) ≤ ( 𝑃 ↑ 𝑁 ) ∧ ( 𝑃 ↑ 𝑁 ) ≤ ( ♯ ‘ 𝐻 ) ) ) )
89	17 83 88	mpbir2and	⊢ ( 𝜑 → ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ 𝑁 ) )
90		fveqeq2	⊢ ( ℎ = 𝐻 → ( ( ♯ ‘ ℎ ) = ( 𝑃 ↑ 𝑁 ) ↔ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ 𝑁 ) ) )
91	90	rspcev	⊢ ( ( 𝐻 ∈ ( SubGrp ‘ 𝐺 ) ∧ ( ♯ ‘ 𝐻 ) = ( 𝑃 ↑ 𝑁 ) ) → ∃ ℎ ∈ ( SubGrp ‘ 𝐺 ) ( ♯ ‘ ℎ ) = ( 𝑃 ↑ 𝑁 ) )
92	16 89 91	syl2anc	⊢ ( 𝜑 → ∃ ℎ ∈ ( SubGrp ‘ 𝐺 ) ( ♯ ‘ ℎ ) = ( 𝑃 ↑ 𝑁 ) )