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 17837 |
. . 3
⊢ (𝜑 → ⊕ ∈ (𝐺 GrpAct 𝑆)) |
11 | | sylow1lem4.b |
. . 3
⊢ (𝜑 → 𝐵 ∈ 𝑆) |
12 | | sylow1lem4.h |
. . . 4
⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐵) = 𝐵} |
13 | 1, 12 | gastacl 17565 |
. . 3
⊢ (( ⊕ ∈
(𝐺 GrpAct 𝑆) ∧ 𝐵 ∈ 𝑆) → 𝐻 ∈ (SubGrp‘𝐺)) |
14 | 10, 11, 13 | syl2anc 691 |
. 2
⊢ (𝜑 → 𝐻 ∈ (SubGrp‘𝐺)) |
15 | | sylow1lem3.1 |
. . . 4
⊢ ∼ =
{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑆 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} |
16 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 15,
11, 12 | sylow1lem4 17839 |
. . 3
⊢ (𝜑 → (#‘𝐻) ≤ (𝑃↑𝑁)) |
17 | | sylow1lem5.l |
. . . . . . . 8
⊢ (𝜑 → (𝑃 pCnt (#‘[𝐵] ∼ )) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁)) |
18 | 15, 1 | gaorber 17564 |
. . . . . . . . . . . . . . . 16
⊢ ( ⊕ ∈
(𝐺 GrpAct 𝑆) → ∼ Er 𝑆) |
19 | 10, 18 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∼ Er 𝑆) |
20 | | erdm 7639 |
. . . . . . . . . . . . . . 15
⊢ ( ∼ Er
𝑆 → dom ∼ =
𝑆) |
21 | 19, 20 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → dom ∼ = 𝑆) |
22 | 11, 21 | eleqtrrd 2691 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐵 ∈ dom ∼ ) |
23 | | ecdmn0 7676 |
. . . . . . . . . . . . 13
⊢ (𝐵 ∈ dom ∼ ↔ [𝐵] ∼ ≠
∅) |
24 | 22, 23 | sylib 207 |
. . . . . . . . . . . 12
⊢ (𝜑 → [𝐵] ∼ ≠
∅) |
25 | | pwfi 8144 |
. . . . . . . . . . . . . . . 16
⊢ (𝑋 ∈ Fin ↔ 𝒫
𝑋 ∈
Fin) |
26 | 3, 25 | sylib 207 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝒫 𝑋 ∈ Fin) |
27 | | ssrab2 3650 |
. . . . . . . . . . . . . . . 16
⊢ {𝑠 ∈ 𝒫 𝑋 ∣ (#‘𝑠) = (𝑃↑𝑁)} ⊆ 𝒫 𝑋 |
28 | 8, 27 | eqsstri 3598 |
. . . . . . . . . . . . . . 15
⊢ 𝑆 ⊆ 𝒫 𝑋 |
29 | | ssfi 8065 |
. . . . . . . . . . . . . . 15
⊢
((𝒫 𝑋 ∈
Fin ∧ 𝑆 ⊆
𝒫 𝑋) → 𝑆 ∈ Fin) |
30 | 26, 28, 29 | sylancl 693 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ∈ Fin) |
31 | 19 | ecss 7675 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → [𝐵] ∼ ⊆ 𝑆) |
32 | | ssfi 8065 |
. . . . . . . . . . . . . 14
⊢ ((𝑆 ∈ Fin ∧ [𝐵] ∼ ⊆ 𝑆) → [𝐵] ∼ ∈
Fin) |
33 | 30, 31, 32 | syl2anc 691 |
. . . . . . . . . . . . 13
⊢ (𝜑 → [𝐵] ∼ ∈
Fin) |
34 | | hashnncl 13018 |
. . . . . . . . . . . . 13
⊢ ([𝐵] ∼ ∈ Fin →
((#‘[𝐵] ∼ )
∈ ℕ ↔ [𝐵]
∼
≠ ∅)) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((#‘[𝐵] ∼ ) ∈ ℕ
↔ [𝐵] ∼ ≠
∅)) |
36 | 24, 35 | mpbird 246 |
. . . . . . . . . . 11
⊢ (𝜑 → (#‘[𝐵] ∼ ) ∈
ℕ) |
37 | 4, 36 | pccld 15393 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑃 pCnt (#‘[𝐵] ∼ )) ∈
ℕ0) |
38 | 37 | nn0red 11229 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃 pCnt (#‘[𝐵] ∼ )) ∈
ℝ) |
39 | 5 | nn0red 11229 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ ℝ) |
40 | 1 | grpbn0 17274 |
. . . . . . . . . . . . 13
⊢ (𝐺 ∈ Grp → 𝑋 ≠ ∅) |
41 | 2, 40 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑋 ≠ ∅) |
42 | | hashnncl 13018 |
. . . . . . . . . . . . 13
⊢ (𝑋 ∈ Fin →
((#‘𝑋) ∈ ℕ
↔ 𝑋 ≠
∅)) |
43 | 3, 42 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → ((#‘𝑋) ∈ ℕ ↔ 𝑋 ≠ ∅)) |
44 | 41, 43 | mpbird 246 |
. . . . . . . . . . 11
⊢ (𝜑 → (#‘𝑋) ∈ ℕ) |
45 | 4, 44 | pccld 15393 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑃 pCnt (#‘𝑋)) ∈
ℕ0) |
46 | 45 | nn0red 11229 |
. . . . . . . . 9
⊢ (𝜑 → (𝑃 pCnt (#‘𝑋)) ∈ ℝ) |
47 | | leaddsub 10383 |
. . . . . . . . 9
⊢ (((𝑃 pCnt (#‘[𝐵] ∼ )) ∈ ℝ
∧ 𝑁 ∈ ℝ
∧ (𝑃 pCnt
(#‘𝑋)) ∈
ℝ) → (((𝑃 pCnt
(#‘[𝐵] ∼ )) +
𝑁) ≤ (𝑃 pCnt (#‘𝑋)) ↔ (𝑃 pCnt (#‘[𝐵] ∼ )) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁))) |
48 | 38, 39, 46, 47 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝜑 → (((𝑃 pCnt (#‘[𝐵] ∼ )) + 𝑁) ≤ (𝑃 pCnt (#‘𝑋)) ↔ (𝑃 pCnt (#‘[𝐵] ∼ )) ≤ ((𝑃 pCnt (#‘𝑋)) − 𝑁))) |
49 | 17, 48 | mpbird 246 |
. . . . . . 7
⊢ (𝜑 → ((𝑃 pCnt (#‘[𝐵] ∼ )) + 𝑁) ≤ (𝑃 pCnt (#‘𝑋))) |
50 | | eqid 2610 |
. . . . . . . . . . 11
⊢ (𝐺 ~QG 𝐻) = (𝐺 ~QG 𝐻) |
51 | 1, 12, 50, 15 | orbsta2 17570 |
. . . . . . . . . 10
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑆) ∧ 𝐵 ∈ 𝑆) ∧ 𝑋 ∈ Fin) → (#‘𝑋) = ((#‘[𝐵] ∼ ) ·
(#‘𝐻))) |
52 | 10, 11, 3, 51 | syl21anc 1317 |
. . . . . . . . 9
⊢ (𝜑 → (#‘𝑋) = ((#‘[𝐵] ∼ ) ·
(#‘𝐻))) |
53 | 52 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 pCnt (#‘𝑋)) = (𝑃 pCnt ((#‘[𝐵] ∼ ) ·
(#‘𝐻)))) |
54 | 36 | nnzd 11357 |
. . . . . . . . 9
⊢ (𝜑 → (#‘[𝐵] ∼ ) ∈
ℤ) |
55 | 36 | nnne0d 10942 |
. . . . . . . . 9
⊢ (𝜑 → (#‘[𝐵] ∼ ) ≠
0) |
56 | | eqid 2610 |
. . . . . . . . . . . . . 14
⊢
(0g‘𝐺) = (0g‘𝐺) |
57 | 56 | subg0cl 17425 |
. . . . . . . . . . . . 13
⊢ (𝐻 ∈ (SubGrp‘𝐺) →
(0g‘𝐺)
∈ 𝐻) |
58 | 14, 57 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝜑 → (0g‘𝐺) ∈ 𝐻) |
59 | | ne0i 3880 |
. . . . . . . . . . . 12
⊢
((0g‘𝐺) ∈ 𝐻 → 𝐻 ≠ ∅) |
60 | 58, 59 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐻 ≠ ∅) |
61 | | ssrab2 3650 |
. . . . . . . . . . . . . 14
⊢ {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐵) = 𝐵} ⊆ 𝑋 |
62 | 12, 61 | eqsstri 3598 |
. . . . . . . . . . . . 13
⊢ 𝐻 ⊆ 𝑋 |
63 | | ssfi 8065 |
. . . . . . . . . . . . 13
⊢ ((𝑋 ∈ Fin ∧ 𝐻 ⊆ 𝑋) → 𝐻 ∈ Fin) |
64 | 3, 62, 63 | sylancl 693 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐻 ∈ Fin) |
65 | | hashnncl 13018 |
. . . . . . . . . . . 12
⊢ (𝐻 ∈ Fin →
((#‘𝐻) ∈ ℕ
↔ 𝐻 ≠
∅)) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . 11
⊢ (𝜑 → ((#‘𝐻) ∈ ℕ ↔ 𝐻 ≠ ∅)) |
67 | 60, 66 | mpbird 246 |
. . . . . . . . . 10
⊢ (𝜑 → (#‘𝐻) ∈ ℕ) |
68 | 67 | nnzd 11357 |
. . . . . . . . 9
⊢ (𝜑 → (#‘𝐻) ∈ ℤ) |
69 | 67 | nnne0d 10942 |
. . . . . . . . 9
⊢ (𝜑 → (#‘𝐻) ≠ 0) |
70 | | pcmul 15394 |
. . . . . . . . 9
⊢ ((𝑃 ∈ ℙ ∧
((#‘[𝐵] ∼ )
∈ ℤ ∧ (#‘[𝐵] ∼ ) ≠ 0) ∧
((#‘𝐻) ∈ ℤ
∧ (#‘𝐻) ≠ 0))
→ (𝑃 pCnt
((#‘[𝐵] ∼ )
· (#‘𝐻))) =
((𝑃 pCnt (#‘[𝐵] ∼ )) + (𝑃 pCnt (#‘𝐻)))) |
71 | 4, 54, 55, 68, 69, 70 | syl122anc 1327 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 pCnt ((#‘[𝐵] ∼ ) ·
(#‘𝐻))) = ((𝑃 pCnt (#‘[𝐵] ∼ )) + (𝑃 pCnt (#‘𝐻)))) |
72 | 53, 71 | eqtrd 2644 |
. . . . . . 7
⊢ (𝜑 → (𝑃 pCnt (#‘𝑋)) = ((𝑃 pCnt (#‘[𝐵] ∼ )) + (𝑃 pCnt (#‘𝐻)))) |
73 | 49, 72 | breqtrd 4609 |
. . . . . 6
⊢ (𝜑 → ((𝑃 pCnt (#‘[𝐵] ∼ )) + 𝑁) ≤ ((𝑃 pCnt (#‘[𝐵] ∼ )) + (𝑃 pCnt (#‘𝐻)))) |
74 | 4, 67 | pccld 15393 |
. . . . . . . 8
⊢ (𝜑 → (𝑃 pCnt (#‘𝐻)) ∈
ℕ0) |
75 | 74 | nn0red 11229 |
. . . . . . 7
⊢ (𝜑 → (𝑃 pCnt (#‘𝐻)) ∈ ℝ) |
76 | 39, 75, 38 | leadd2d 10501 |
. . . . . 6
⊢ (𝜑 → (𝑁 ≤ (𝑃 pCnt (#‘𝐻)) ↔ ((𝑃 pCnt (#‘[𝐵] ∼ )) + 𝑁) ≤ ((𝑃 pCnt (#‘[𝐵] ∼ )) + (𝑃 pCnt (#‘𝐻))))) |
77 | 73, 76 | mpbird 246 |
. . . . 5
⊢ (𝜑 → 𝑁 ≤ (𝑃 pCnt (#‘𝐻))) |
78 | | pcdvdsb 15411 |
. . . . . 6
⊢ ((𝑃 ∈ ℙ ∧
(#‘𝐻) ∈ ℤ
∧ 𝑁 ∈
ℕ0) → (𝑁 ≤ (𝑃 pCnt (#‘𝐻)) ↔ (𝑃↑𝑁) ∥ (#‘𝐻))) |
79 | 4, 68, 5, 78 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → (𝑁 ≤ (𝑃 pCnt (#‘𝐻)) ↔ (𝑃↑𝑁) ∥ (#‘𝐻))) |
80 | 77, 79 | mpbid 221 |
. . . 4
⊢ (𝜑 → (𝑃↑𝑁) ∥ (#‘𝐻)) |
81 | | prmnn 15226 |
. . . . . . . 8
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
82 | 4, 81 | syl 17 |
. . . . . . 7
⊢ (𝜑 → 𝑃 ∈ ℕ) |
83 | 82, 5 | nnexpcld 12892 |
. . . . . 6
⊢ (𝜑 → (𝑃↑𝑁) ∈ ℕ) |
84 | 83 | nnzd 11357 |
. . . . 5
⊢ (𝜑 → (𝑃↑𝑁) ∈ ℤ) |
85 | | dvdsle 14870 |
. . . . 5
⊢ (((𝑃↑𝑁) ∈ ℤ ∧ (#‘𝐻) ∈ ℕ) → ((𝑃↑𝑁) ∥ (#‘𝐻) → (𝑃↑𝑁) ≤ (#‘𝐻))) |
86 | 84, 67, 85 | syl2anc 691 |
. . . 4
⊢ (𝜑 → ((𝑃↑𝑁) ∥ (#‘𝐻) → (𝑃↑𝑁) ≤ (#‘𝐻))) |
87 | 80, 86 | mpd 15 |
. . 3
⊢ (𝜑 → (𝑃↑𝑁) ≤ (#‘𝐻)) |
88 | | hashcl 13009 |
. . . . . 6
⊢ (𝐻 ∈ Fin →
(#‘𝐻) ∈
ℕ0) |
89 | 64, 88 | syl 17 |
. . . . 5
⊢ (𝜑 → (#‘𝐻) ∈
ℕ0) |
90 | 89 | nn0red 11229 |
. . . 4
⊢ (𝜑 → (#‘𝐻) ∈ ℝ) |
91 | 83 | nnred 10912 |
. . . 4
⊢ (𝜑 → (𝑃↑𝑁) ∈ ℝ) |
92 | 90, 91 | letri3d 10058 |
. . 3
⊢ (𝜑 → ((#‘𝐻) = (𝑃↑𝑁) ↔ ((#‘𝐻) ≤ (𝑃↑𝑁) ∧ (𝑃↑𝑁) ≤ (#‘𝐻)))) |
93 | 16, 87, 92 | mpbir2and 959 |
. 2
⊢ (𝜑 → (#‘𝐻) = (𝑃↑𝑁)) |
94 | | fveq2 6103 |
. . . 4
⊢ (ℎ = 𝐻 → (#‘ℎ) = (#‘𝐻)) |
95 | 94 | eqeq1d 2612 |
. . 3
⊢ (ℎ = 𝐻 → ((#‘ℎ) = (𝑃↑𝑁) ↔ (#‘𝐻) = (𝑃↑𝑁))) |
96 | 95 | rspcev 3282 |
. 2
⊢ ((𝐻 ∈ (SubGrp‘𝐺) ∧ (#‘𝐻) = (𝑃↑𝑁)) → ∃ℎ ∈ (SubGrp‘𝐺)(#‘ℎ) = (𝑃↑𝑁)) |
97 | 14, 93, 96 | syl2anc 691 |
1
⊢ (𝜑 → ∃ℎ ∈ (SubGrp‘𝐺)(#‘ℎ) = (𝑃↑𝑁)) |