Proof of Theorem sylow1lem5
Step | Hyp | Ref
| Expression |
1 | | sylow1.x |
. . . 4
⊢ 𝑋 = (Base‘𝐺) |
2 | | sylow1.g |
. . . 4
⊢ (𝜑 → 𝐺 ∈ Grp) |
3 | | sylow1.f |
. . . 4
⊢ (𝜑 → 𝑋 ∈ Fin) |
4 | | sylow1.p |
. . . 4
⊢ (𝜑 → 𝑃 ∈ ℙ) |
5 | | sylow1.n |
. . . 4
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
6 | | sylow1.d |
. . . 4
⊢ (𝜑 → (𝑃↑𝑁) ∥ (♯‘𝑋)) |
7 | | sylow1lem.a |
. . . 4
⊢ + =
(+g‘𝐺) |
8 | | sylow1lem.s |
. . . 4
⊢ 𝑆 = {𝑠 ∈ 𝒫 𝑋 ∣ (♯‘𝑠) = (𝑃↑𝑁)} |
9 | | sylow1lem.m |
. . . 4
⊢ ⊕ =
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑆 ↦ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | sylow1lem2 18220 |
. . 3
⊢ (𝜑 → ⊕ ∈ (𝐺 GrpAct 𝑆)) |
11 | | sylow1lem4.b |
. . 3
⊢ (𝜑 → 𝐵 ∈ 𝑆) |
12 | | sylow1lem4.h |
. . . 4
⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐵) = 𝐵} |
13 | 1, 12 | gastacl 17948 |
. . 3
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑆) ∧ 𝐵 ∈ 𝑆) → 𝐻 ∈ (SubGrp‘𝐺)) |
14 | 10, 11, 13 | syl2anc 565 |
. 2
⊢ (𝜑 → 𝐻 ∈ (SubGrp‘𝐺)) |
15 | | sylow1lem3.1 |
. . . 4
⊢ ∼ =
{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑆 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} |
16 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 15,
11, 12 | sylow1lem4 18222 |
. . 3
⊢ (𝜑 → (♯‘𝐻) ≤ (𝑃↑𝑁)) |
17 | | sylow1lem5.l |
. . . . . . . 8
⊢ (𝜑 → (𝑃 pCnt (♯‘[𝐵] ∼ )) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁)) |
18 | 15, 1 | gaorber 17947 |
. . . . . . . . . . . . . . . 16
⊢ ( ⊕ ∈
(𝐺 GrpAct 𝑆) → ∼ Er 𝑆) |
19 | 10, 18 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∼ Er 𝑆) |
20 | | erdm 7905 |
. . . . . . . . . . . . . . 15
⊢ ( ∼ Er
𝑆 → dom ∼ =
𝑆) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom ∼ = 𝑆) |
22 | 11, 21 | eleqtrrd 2853 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ dom ∼ ) |
23 | | ecdmn0 7940 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ dom ∼ ↔ [𝐵] ∼ ≠
∅) |
24 | 22, 23 | sylib 208 |
. . . . . . . . . . . 12
⊢ (𝜑 → [𝐵] ∼ ≠
∅) |
25 | | pwfi 8416 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 ∈ Fin ↔ 𝒫
𝑋 ∈
Fin) |
26 | 3, 25 | sylib 208 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝒫 𝑋 ∈ Fin) |
27 | | ssrab2 3836 |
. . . . . . . . . . . . . . . 16
⊢ {𝑠 ∈ 𝒫 𝑋 ∣ (♯‘𝑠) = (𝑃↑𝑁)} ⊆ 𝒫 𝑋 |
28 | 8, 27 | eqsstri 3784 |
. . . . . . . . . . . . . . 15
⊢ 𝑆 ⊆ 𝒫 𝑋 |
29 | | ssfi 8335 |
. . . . . . . . . . . . . . 15
⊢
((𝒫 𝑋 ∈
Fin ∧ 𝑆 ⊆
𝒫 𝑋) → 𝑆 ∈ Fin) |
30 | 26, 28, 29 | sylancl 566 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ∈ Fin) |
31 | 19 | ecss 7939 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → [𝐵] ∼ ⊆ 𝑆) |
32 | | ssfi 8335 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ Fin ∧ [𝐵] ∼ ⊆ 𝑆) → [𝐵] ∼ ∈
Fin) |
33 | 30, 31, 32 | syl2anc 565 |
. . . . . . . . . . . . 13
⊢ (𝜑 → [𝐵] ∼ ∈
Fin) |
34 | | hashnncl 13358 |
. . . . . . . . . . . . 13
⊢ ([𝐵] ∼ ∈ Fin →
((♯‘[𝐵] ∼ )
∈ ℕ ↔ [𝐵]
∼
≠ ∅)) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((♯‘[𝐵] ∼ ) ∈ ℕ
↔ [𝐵] ∼ ≠
∅)) |
36 | 24, 35 | mpbird 247 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘[𝐵] ∼ ) ∈
ℕ) |
37 | 4, 36 | pccld 15761 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑃 pCnt (♯‘[𝐵] ∼ )) ∈
ℕ0) |
38 | 37 | nn0red 11553 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃 pCnt (♯‘[𝐵] ∼ )) ∈
ℝ) |
39 | 5 | nn0red 11553 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℝ) |
40 | 1 | grpbn0 17658 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ Grp → 𝑋 ≠ ∅) |
41 | 2, 40 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ≠ ∅) |
42 | | hashnncl 13358 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ Fin →
((♯‘𝑋) ∈
ℕ ↔ 𝑋 ≠
∅)) |
43 | 3, 42 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((♯‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅)) |
44 | 41, 43 | mpbird 247 |
. . . . . . . . . . 11
⊢ (𝜑 → (♯‘𝑋) ∈
ℕ) |
45 | 4, 44 | pccld 15761 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑃 pCnt (♯‘𝑋)) ∈
ℕ0) |
46 | 45 | nn0red 11553 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃 pCnt (♯‘𝑋)) ∈ ℝ) |
47 | | leaddsub 10705 |
. . . . . . . . 9
⊢ (((𝑃 pCnt (♯‘[𝐵] ∼ )) ∈ ℝ
∧ 𝑁 ∈ ℝ
∧ (𝑃 pCnt
(♯‘𝑋)) ∈
ℝ) → (((𝑃 pCnt
(♯‘[𝐵] ∼ )) +
𝑁) ≤ (𝑃 pCnt (♯‘𝑋)) ↔ (𝑃 pCnt (♯‘[𝐵] ∼ )) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁))) |
48 | 38, 39, 46, 47 | syl3anc 1476 |
. . . . . . . 8
⊢ (𝜑 → (((𝑃 pCnt (♯‘[𝐵] ∼ )) + 𝑁) ≤ (𝑃 pCnt (♯‘𝑋)) ↔ (𝑃 pCnt (♯‘[𝐵] ∼ )) ≤ ((𝑃 pCnt (♯‘𝑋)) − 𝑁))) |
49 | 17, 48 | mpbird 247 |
. . . . . . 7
⊢ (𝜑 → ((𝑃 pCnt (♯‘[𝐵] ∼ )) + 𝑁) ≤ (𝑃 pCnt (♯‘𝑋))) |
50 | | eqid 2771 |
. . . . . . . . . . 11
⊢ (𝐺 ~QG 𝐻) = (𝐺 ~QG 𝐻) |
51 | 1, 12, 50, 15 | orbsta2 17953 |
. . . . . . . . . 10
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑆) ∧ 𝐵 ∈ 𝑆) ∧ 𝑋 ∈ Fin) → (♯‘𝑋) = ((♯‘[𝐵] ∼ ) ·
(♯‘𝐻))) |
52 | 10, 11, 3, 51 | syl21anc 1475 |
. . . . . . . . 9
⊢ (𝜑 → (♯‘𝑋) = ((♯‘[𝐵] ∼ ) ·
(♯‘𝐻))) |
53 | 52 | oveq2d 6808 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 pCnt (♯‘𝑋)) = (𝑃 pCnt ((♯‘[𝐵] ∼ ) ·
(♯‘𝐻)))) |
54 | 36 | nnzd 11682 |
. . . . . . . . 9
⊢ (𝜑 → (♯‘[𝐵] ∼ ) ∈
ℤ) |
55 | 36 | nnne0d 11266 |
. . . . . . . . 9
⊢ (𝜑 → (♯‘[𝐵] ∼ ) ≠
0) |
56 | | eqid 2771 |
. . . . . . . . . . . . . 14
⊢
(0g‘𝐺) = (0g‘𝐺) |
57 | 56 | subg0cl 17809 |
. . . . . . . . . . . . 13
⊢ (𝐻 ∈ (SubGrp‘𝐺) →
(0g‘𝐺)
∈ 𝐻) |
58 | 14, 57 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0g‘𝐺) ∈ 𝐻) |
59 | | ne0i 4069 |
. . . . . . . . . . . 12
⊢
((0g‘𝐺) ∈ 𝐻 → 𝐻 ≠ ∅) |
60 | 58, 59 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐻 ≠ ∅) |
61 | | ssrab2 3836 |
. . . . . . . . . . . . . 14
⊢ {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐵) = 𝐵} ⊆ 𝑋 |
62 | 12, 61 | eqsstri 3784 |
. . . . . . . . . . . . 13
⊢ 𝐻 ⊆ 𝑋 |
63 | | ssfi 8335 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ Fin ∧ 𝐻 ⊆ 𝑋) → 𝐻 ∈ Fin) |
64 | 3, 62, 63 | sylancl 566 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐻 ∈ Fin) |
65 | | hashnncl 13358 |
. . . . . . . . . . . 12
⊢ (𝐻 ∈ Fin →
((♯‘𝐻) ∈
ℕ ↔ 𝐻 ≠
∅)) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((♯‘𝐻) ∈ ℕ ↔ 𝐻 ≠ ∅)) |
67 | 60, 66 | mpbird 247 |
. . . . . . . . . 10
⊢ (𝜑 → (♯‘𝐻) ∈
ℕ) |
68 | 67 | nnzd 11682 |
. . . . . . . . 9
⊢ (𝜑 → (♯‘𝐻) ∈
ℤ) |
69 | 67 | nnne0d 11266 |
. . . . . . . . 9
⊢ (𝜑 → (♯‘𝐻) ≠ 0) |
70 | | pcmul 15762 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧
((♯‘[𝐵] ∼ )
∈ ℤ ∧ (♯‘[𝐵] ∼ ) ≠ 0) ∧
((♯‘𝐻) ∈
ℤ ∧ (♯‘𝐻) ≠ 0)) → (𝑃 pCnt ((♯‘[𝐵] ∼ ) ·
(♯‘𝐻))) =
((𝑃 pCnt
(♯‘[𝐵] ∼ )) +
(𝑃 pCnt
(♯‘𝐻)))) |
71 | 4, 54, 55, 68, 69, 70 | syl122anc 1485 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 pCnt ((♯‘[𝐵] ∼ ) ·
(♯‘𝐻))) =
((𝑃 pCnt
(♯‘[𝐵] ∼ )) +
(𝑃 pCnt
(♯‘𝐻)))) |
72 | 53, 71 | eqtrd 2805 |
. . . . . . 7
⊢ (𝜑 → (𝑃 pCnt (♯‘𝑋)) = ((𝑃 pCnt (♯‘[𝐵] ∼ )) + (𝑃 pCnt (♯‘𝐻)))) |
73 | 49, 72 | breqtrd 4812 |
. . . . . 6
⊢ (𝜑 → ((𝑃 pCnt (♯‘[𝐵] ∼ )) + 𝑁) ≤ ((𝑃 pCnt (♯‘[𝐵] ∼ )) + (𝑃 pCnt (♯‘𝐻)))) |
74 | 4, 67 | pccld 15761 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 pCnt (♯‘𝐻)) ∈
ℕ0) |
75 | 74 | nn0red 11553 |
. . . . . . 7
⊢ (𝜑 → (𝑃 pCnt (♯‘𝐻)) ∈ ℝ) |
76 | 39, 75, 38 | leadd2d 10823 |
. . . . . 6
⊢ (𝜑 → (𝑁 ≤ (𝑃 pCnt (♯‘𝐻)) ↔ ((𝑃 pCnt (♯‘[𝐵] ∼ )) + 𝑁) ≤ ((𝑃 pCnt (♯‘[𝐵] ∼ )) + (𝑃 pCnt (♯‘𝐻))))) |
77 | 73, 76 | mpbird 247 |
. . . . 5
⊢ (𝜑 → 𝑁 ≤ (𝑃 pCnt (♯‘𝐻))) |
78 | | pcdvdsb 15779 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧
(♯‘𝐻) ∈
ℤ ∧ 𝑁 ∈
ℕ0) → (𝑁 ≤ (𝑃 pCnt (♯‘𝐻)) ↔ (𝑃↑𝑁) ∥ (♯‘𝐻))) |
79 | 4, 68, 5, 78 | syl3anc 1476 |
. . . . 5
⊢ (𝜑 → (𝑁 ≤ (𝑃 pCnt (♯‘𝐻)) ↔ (𝑃↑𝑁) ∥ (♯‘𝐻))) |
80 | 77, 79 | mpbid 222 |
. . . 4
⊢ (𝜑 → (𝑃↑𝑁) ∥ (♯‘𝐻)) |
81 | | prmnn 15594 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
82 | 4, 81 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ ℕ) |
83 | 82, 5 | nnexpcld 13236 |
. . . . . 6
⊢ (𝜑 → (𝑃↑𝑁) ∈ ℕ) |
84 | 83 | nnzd 11682 |
. . . . 5
⊢ (𝜑 → (𝑃↑𝑁) ∈ ℤ) |
85 | | dvdsle 15240 |
. . . . 5
⊢ (((𝑃↑𝑁) ∈ ℤ ∧ (♯‘𝐻) ∈ ℕ) → ((𝑃↑𝑁) ∥ (♯‘𝐻) → (𝑃↑𝑁) ≤ (♯‘𝐻))) |
86 | 84, 67, 85 | syl2anc 565 |
. . . 4
⊢ (𝜑 → ((𝑃↑𝑁) ∥ (♯‘𝐻) → (𝑃↑𝑁) ≤ (♯‘𝐻))) |
87 | 80, 86 | mpd 15 |
. . 3
⊢ (𝜑 → (𝑃↑𝑁) ≤ (♯‘𝐻)) |
88 | | hashcl 13348 |
. . . . . 6
⊢ (𝐻 ∈ Fin →
(♯‘𝐻) ∈
ℕ0) |
89 | 64, 88 | syl 17 |
. . . . 5
⊢ (𝜑 → (♯‘𝐻) ∈
ℕ0) |
90 | 89 | nn0red 11553 |
. . . 4
⊢ (𝜑 → (♯‘𝐻) ∈
ℝ) |
91 | 83 | nnred 11236 |
. . . 4
⊢ (𝜑 → (𝑃↑𝑁) ∈ ℝ) |
92 | 90, 91 | letri3d 10380 |
. . 3
⊢ (𝜑 → ((♯‘𝐻) = (𝑃↑𝑁) ↔ ((♯‘𝐻) ≤ (𝑃↑𝑁) ∧ (𝑃↑𝑁) ≤ (♯‘𝐻)))) |
93 | 16, 87, 92 | mpbir2and 684 |
. 2
⊢ (𝜑 → (♯‘𝐻) = (𝑃↑𝑁)) |
94 | | fveq2 6332 |
. . . 4
⊢ (ℎ = 𝐻 → (♯‘ℎ) = (♯‘𝐻)) |
95 | 94 | eqeq1d 2773 |
. . 3
⊢ (ℎ = 𝐻 → ((♯‘ℎ) = (𝑃↑𝑁) ↔ (♯‘𝐻) = (𝑃↑𝑁))) |
96 | 95 | rspcev 3460 |
. 2
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ (♯‘𝐻) = (𝑃↑𝑁)) → ∃ℎ ∈ (SubGrp‘𝐺)(♯‘ℎ) = (𝑃↑𝑁)) |
97 | 14, 93, 96 | syl2anc 565 |
1
⊢ (𝜑 → ∃ℎ ∈ (SubGrp‘𝐺)(♯‘ℎ) = (𝑃↑𝑁)) |