This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝐺 ) ( ♯ ‘ ℎ ) = ( 𝑃 ↑ 𝑁 ) )