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 18014 |
. . 3
⊢ (𝜑 → ⊕ ∈ (𝐺 GrpAct 𝑆)) |
11 | | sylow1lem4.b |
. . 3
⊢ (𝜑 → 𝐵 ∈ 𝑆) |
12 | | sylow1lem4.h |
. . . 4
⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐵) = 𝐵} |
13 | 1, 12 | gastacl 17742 |
. . 3
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑆) ∧ 𝐵 ∈ 𝑆) → 𝐻 ∈ (SubGrp‘𝐺)) |
14 | 10, 11, 13 | syl2anc 693 |
. 2
⊢ (𝜑 → 𝐻 ∈ (SubGrp‘𝐺)) |
15 | | sylow1lem3.1 |
. . . 4
⊢ ∼ =
{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑆 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} |
16 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 15,
11, 12 | sylow1lem4 18016 |
. . 3
⊢ (𝜑 → (#‘𝐻) ≤ (𝑃↑𝑁)) |
17 | | sylow1lem5.l |
. . . . . . . 8
⊢ (𝜑 → (𝑃 pCnt (#‘[𝐵] ∼ )) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁)) |
18 | 15, 1 | gaorber 17741 |
. . . . . . . . . . . . . . . 16
⊢ ( ⊕ ∈
(𝐺 GrpAct 𝑆) → ∼ Er 𝑆) |
19 | 10, 18 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∼ Er 𝑆) |
20 | | erdm 7752 |
. . . . . . . . . . . . . . 15
⊢ ( ∼ Er
𝑆 → dom ∼ =
𝑆) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom ∼ = 𝑆) |
22 | 11, 21 | eleqtrrd 2704 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ dom ∼ ) |
23 | | ecdmn0 7789 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ dom ∼ ↔ [𝐵] ∼ ≠
∅) |
24 | 22, 23 | sylib 208 |
. . . . . . . . . . . 12
⊢ (𝜑 → [𝐵] ∼ ≠
∅) |
25 | | pwfi 8261 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 ∈ Fin ↔ 𝒫
𝑋 ∈
Fin) |
26 | 3, 25 | sylib 208 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝒫 𝑋 ∈ Fin) |
27 | | ssrab2 3687 |
. . . . . . . . . . . . . . . 16
⊢ {𝑠 ∈ 𝒫 𝑋 ∣ (#‘𝑠) = (𝑃↑𝑁)} ⊆ 𝒫 𝑋 |
28 | 8, 27 | eqsstri 3635 |
. . . . . . . . . . . . . . 15
⊢ 𝑆 ⊆ 𝒫 𝑋 |
29 | | ssfi 8180 |
. . . . . . . . . . . . . . 15
⊢
((𝒫 𝑋 ∈
Fin ∧ 𝑆 ⊆
𝒫 𝑋) → 𝑆 ∈ Fin) |
30 | 26, 28, 29 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ∈ Fin) |
31 | 19 | ecss 7788 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → [𝐵] ∼ ⊆ 𝑆) |
32 | | ssfi 8180 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ Fin ∧ [𝐵] ∼ ⊆ 𝑆) → [𝐵] ∼ ∈
Fin) |
33 | 30, 31, 32 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ (𝜑 → [𝐵] ∼ ∈
Fin) |
34 | | hashnncl 13157 |
. . . . . . . . . . . . 13
⊢ ([𝐵] ∼ ∈ Fin →
((#‘[𝐵] ∼ )
∈ ℕ ↔ [𝐵]
∼
≠ ∅)) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((#‘[𝐵] ∼ ) ∈ ℕ
↔ [𝐵] ∼ ≠
∅)) |
36 | 24, 35 | mpbird 247 |
. . . . . . . . . . 11
⊢ (𝜑 → (#‘[𝐵] ∼ ) ∈
ℕ) |
37 | 4, 36 | pccld 15555 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑃 pCnt (#‘[𝐵] ∼ )) ∈
ℕ0) |
38 | 37 | nn0red 11352 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃 pCnt (#‘[𝐵] ∼ )) ∈
ℝ) |
39 | 5 | nn0red 11352 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℝ) |
40 | 1 | grpbn0 17451 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ Grp → 𝑋 ≠ ∅) |
41 | 2, 40 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ≠ ∅) |
42 | | hashnncl 13157 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ Fin →
((#‘𝑋) ∈ ℕ
↔ 𝑋 ≠
∅)) |
43 | 3, 42 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((#‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅)) |
44 | 41, 43 | mpbird 247 |
. . . . . . . . . . 11
⊢ (𝜑 → (#‘𝑋) ∈ ℕ) |
45 | 4, 44 | pccld 15555 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑃 pCnt (#‘𝑋)) ∈
ℕ0) |
46 | 45 | nn0red 11352 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃 pCnt (#‘𝑋)) ∈ ℝ) |
47 | | leaddsub 10504 |
. . . . . . . . 9
⊢ (((𝑃 pCnt (#‘[𝐵] ∼ )) ∈ ℝ
∧ 𝑁 ∈ ℝ
∧ (𝑃 pCnt
(#‘𝑋)) ∈
ℝ) → (((𝑃 pCnt
(#‘[𝐵] ∼ )) +
𝑁) ≤ (𝑃 pCnt (#‘𝑋)) ↔ (𝑃 pCnt (#‘[𝐵] ∼ )) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁))) |
48 | 38, 39, 46, 47 | syl3anc 1326 |
. . . . . . . 8
⊢ (𝜑 → (((𝑃 pCnt (#‘[𝐵] ∼ )) + 𝑁) ≤ (𝑃 pCnt (#‘𝑋)) ↔ (𝑃 pCnt (#‘[𝐵] ∼ )) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁))) |
49 | 17, 48 | mpbird 247 |
. . . . . . 7
⊢ (𝜑 → ((𝑃 pCnt (#‘[𝐵] ∼ )) + 𝑁) ≤ (𝑃 pCnt (#‘𝑋))) |
50 | | eqid 2622 |
. . . . . . . . . . 11
⊢ (𝐺 ~QG 𝐻) = (𝐺 ~QG 𝐻) |
51 | 1, 12, 50, 15 | orbsta2 17747 |
. . . . . . . . . 10
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑆) ∧ 𝐵 ∈ 𝑆) ∧ 𝑋 ∈ Fin) → (#‘𝑋) = ((#‘[𝐵] ∼ ) ·
(#‘𝐻))) |
52 | 10, 11, 3, 51 | syl21anc 1325 |
. . . . . . . . 9
⊢ (𝜑 → (#‘𝑋) = ((#‘[𝐵] ∼ ) ·
(#‘𝐻))) |
53 | 52 | oveq2d 6666 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 pCnt (#‘𝑋)) = (𝑃 pCnt ((#‘[𝐵] ∼ ) ·
(#‘𝐻)))) |
54 | 36 | nnzd 11481 |
. . . . . . . . 9
⊢ (𝜑 → (#‘[𝐵] ∼ ) ∈
ℤ) |
55 | 36 | nnne0d 11065 |
. . . . . . . . 9
⊢ (𝜑 → (#‘[𝐵] ∼ ) ≠
0) |
56 | | eqid 2622 |
. . . . . . . . . . . . . 14
⊢
(0g‘𝐺) = (0g‘𝐺) |
57 | 56 | subg0cl 17602 |
. . . . . . . . . . . . 13
⊢ (𝐻 ∈ (SubGrp‘𝐺) →
(0g‘𝐺)
∈ 𝐻) |
58 | 14, 57 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0g‘𝐺) ∈ 𝐻) |
59 | | ne0i 3921 |
. . . . . . . . . . . 12
⊢
((0g‘𝐺) ∈ 𝐻 → 𝐻 ≠ ∅) |
60 | 58, 59 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐻 ≠ ∅) |
61 | | ssrab2 3687 |
. . . . . . . . . . . . . 14
⊢ {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐵) = 𝐵} ⊆ 𝑋 |
62 | 12, 61 | eqsstri 3635 |
. . . . . . . . . . . . 13
⊢ 𝐻 ⊆ 𝑋 |
63 | | ssfi 8180 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ Fin ∧ 𝐻 ⊆ 𝑋) → 𝐻 ∈ Fin) |
64 | 3, 62, 63 | sylancl 694 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐻 ∈ Fin) |
65 | | hashnncl 13157 |
. . . . . . . . . . . 12
⊢ (𝐻 ∈ Fin →
((#‘𝐻) ∈ ℕ
↔ 𝐻 ≠
∅)) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((#‘𝐻) ∈ ℕ ↔ 𝐻 ≠ ∅)) |
67 | 60, 66 | mpbird 247 |
. . . . . . . . . 10
⊢ (𝜑 → (#‘𝐻) ∈ ℕ) |
68 | 67 | nnzd 11481 |
. . . . . . . . 9
⊢ (𝜑 → (#‘𝐻) ∈ ℤ) |
69 | 67 | nnne0d 11065 |
. . . . . . . . 9
⊢ (𝜑 → (#‘𝐻) ≠ 0) |
70 | | pcmul 15556 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧
((#‘[𝐵] ∼ )
∈ ℤ ∧ (#‘[𝐵] ∼ ) ≠ 0) ∧
((#‘𝐻) ∈ ℤ
∧ (#‘𝐻) ≠ 0))
→ (𝑃 pCnt
((#‘[𝐵] ∼ )
· (#‘𝐻))) =
((𝑃 pCnt (#‘[𝐵] ∼ )) + (𝑃 pCnt (#‘𝐻)))) |
71 | 4, 54, 55, 68, 69, 70 | syl122anc 1335 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 pCnt ((#‘[𝐵] ∼ ) ·
(#‘𝐻))) = ((𝑃 pCnt (#‘[𝐵] ∼ )) + (𝑃 pCnt (#‘𝐻)))) |
72 | 53, 71 | eqtrd 2656 |
. . . . . . 7
⊢ (𝜑 → (𝑃 pCnt (#‘𝑋)) = ((𝑃 pCnt (#‘[𝐵] ∼ )) + (𝑃 pCnt (#‘𝐻)))) |
73 | 49, 72 | breqtrd 4679 |
. . . . . 6
⊢ (𝜑 → ((𝑃 pCnt (#‘[𝐵] ∼ )) + 𝑁) ≤ ((𝑃 pCnt (#‘[𝐵] ∼ )) + (𝑃 pCnt (#‘𝐻)))) |
74 | 4, 67 | pccld 15555 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 pCnt (#‘𝐻)) ∈
ℕ0) |
75 | 74 | nn0red 11352 |
. . . . . . 7
⊢ (𝜑 → (𝑃 pCnt (#‘𝐻)) ∈ ℝ) |
76 | 39, 75, 38 | leadd2d 10622 |
. . . . . 6
⊢ (𝜑 → (𝑁 ≤ (𝑃 pCnt (#‘𝐻)) ↔ ((𝑃 pCnt (#‘[𝐵] ∼ )) + 𝑁) ≤ ((𝑃 pCnt (#‘[𝐵] ∼ )) + (𝑃 pCnt (#‘𝐻))))) |
77 | 73, 76 | mpbird 247 |
. . . . 5
⊢ (𝜑 → 𝑁 ≤ (𝑃 pCnt (#‘𝐻))) |
78 | | pcdvdsb 15573 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧
(#‘𝐻) ∈ ℤ
∧ 𝑁 ∈
ℕ0) → (𝑁 ≤ (𝑃 pCnt (#‘𝐻)) ↔ (𝑃↑𝑁) ∥ (#‘𝐻))) |
79 | 4, 68, 5, 78 | syl3anc 1326 |
. . . . 5
⊢ (𝜑 → (𝑁 ≤ (𝑃 pCnt (#‘𝐻)) ↔ (𝑃↑𝑁) ∥ (#‘𝐻))) |
80 | 77, 79 | mpbid 222 |
. . . 4
⊢ (𝜑 → (𝑃↑𝑁) ∥ (#‘𝐻)) |
81 | | prmnn 15388 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
82 | 4, 81 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ ℕ) |
83 | 82, 5 | nnexpcld 13030 |
. . . . . 6
⊢ (𝜑 → (𝑃↑𝑁) ∈ ℕ) |
84 | 83 | nnzd 11481 |
. . . . 5
⊢ (𝜑 → (𝑃↑𝑁) ∈ ℤ) |
85 | | dvdsle 15032 |
. . . . 5
⊢ (((𝑃↑𝑁) ∈ ℤ ∧ (#‘𝐻) ∈ ℕ) → ((𝑃↑𝑁) ∥ (#‘𝐻) → (𝑃↑𝑁) ≤ (#‘𝐻))) |
86 | 84, 67, 85 | syl2anc 693 |
. . . 4
⊢ (𝜑 → ((𝑃↑𝑁) ∥ (#‘𝐻) → (𝑃↑𝑁) ≤ (#‘𝐻))) |
87 | 80, 86 | mpd 15 |
. . 3
⊢ (𝜑 → (𝑃↑𝑁) ≤ (#‘𝐻)) |
88 | | hashcl 13147 |
. . . . . 6
⊢ (𝐻 ∈ Fin →
(#‘𝐻) ∈
ℕ0) |
89 | 64, 88 | syl 17 |
. . . . 5
⊢ (𝜑 → (#‘𝐻) ∈
ℕ0) |
90 | 89 | nn0red 11352 |
. . . 4
⊢ (𝜑 → (#‘𝐻) ∈ ℝ) |
91 | 83 | nnred 11035 |
. . . 4
⊢ (𝜑 → (𝑃↑𝑁) ∈ ℝ) |
92 | 90, 91 | letri3d 10179 |
. . 3
⊢ (𝜑 → ((#‘𝐻) = (𝑃↑𝑁) ↔ ((#‘𝐻) ≤ (𝑃↑𝑁) ∧ (𝑃↑𝑁) ≤ (#‘𝐻)))) |
93 | 16, 87, 92 | mpbir2and 957 |
. 2
⊢ (𝜑 → (#‘𝐻) = (𝑃↑𝑁)) |
94 | | fveq2 6191 |
. . . 4
⊢ (ℎ = 𝐻 → (#‘ℎ) = (#‘𝐻)) |
95 | 94 | eqeq1d 2624 |
. . 3
⊢ (ℎ = 𝐻 → ((#‘ℎ) = (𝑃↑𝑁) ↔ (#‘𝐻) = (𝑃↑𝑁))) |
96 | 95 | rspcev 3309 |
. 2
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ (#‘𝐻) = (𝑃↑𝑁)) → ∃ℎ ∈ (SubGrp‘𝐺)(#‘ℎ) = (𝑃↑𝑁)) |
97 | 14, 93, 96 | syl2anc 693 |
1
⊢ (𝜑 → ∃ℎ ∈ (SubGrp‘𝐺)(#‘ℎ) = (𝑃↑𝑁)) |