Step | Hyp | Ref
| Expression |
1 | | sylow1lem4.b |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ∈ 𝑆) |
2 | | fveq2 6191 |
. . . . . . . . . . . 12
⊢ (𝑠 = 𝐵 → (#‘𝑠) = (#‘𝐵)) |
3 | 2 | eqeq1d 2624 |
. . . . . . . . . . 11
⊢ (𝑠 = 𝐵 → ((#‘𝑠) = (𝑃↑𝑁) ↔ (#‘𝐵) = (𝑃↑𝑁))) |
4 | | sylow1lem.s |
. . . . . . . . . . 11
⊢ 𝑆 = {𝑠 ∈ 𝒫 𝑋 ∣ (#‘𝑠) = (𝑃↑𝑁)} |
5 | 3, 4 | elrab2 3366 |
. . . . . . . . . 10
⊢ (𝐵 ∈ 𝑆 ↔ (𝐵 ∈ 𝒫 𝑋 ∧ (#‘𝐵) = (𝑃↑𝑁))) |
6 | 1, 5 | sylib 208 |
. . . . . . . . 9
⊢ (𝜑 → (𝐵 ∈ 𝒫 𝑋 ∧ (#‘𝐵) = (𝑃↑𝑁))) |
7 | 6 | simprd 479 |
. . . . . . . 8
⊢ (𝜑 → (#‘𝐵) = (𝑃↑𝑁)) |
8 | | sylow1.p |
. . . . . . . . . 10
⊢ (𝜑 → 𝑃 ∈ ℙ) |
9 | | prmnn 15388 |
. . . . . . . . . 10
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℕ) |
10 | 8, 9 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → 𝑃 ∈ ℕ) |
11 | | sylow1.n |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
12 | 10, 11 | nnexpcld 13030 |
. . . . . . . 8
⊢ (𝜑 → (𝑃↑𝑁) ∈ ℕ) |
13 | 7, 12 | eqeltrd 2701 |
. . . . . . 7
⊢ (𝜑 → (#‘𝐵) ∈ ℕ) |
14 | 13 | nnne0d 11065 |
. . . . . 6
⊢ (𝜑 → (#‘𝐵) ≠ 0) |
15 | | hasheq0 13154 |
. . . . . . . 8
⊢ (𝐵 ∈ 𝑆 → ((#‘𝐵) = 0 ↔ 𝐵 = ∅)) |
16 | 15 | necon3bid 2838 |
. . . . . . 7
⊢ (𝐵 ∈ 𝑆 → ((#‘𝐵) ≠ 0 ↔ 𝐵 ≠ ∅)) |
17 | 1, 16 | syl 17 |
. . . . . 6
⊢ (𝜑 → ((#‘𝐵) ≠ 0 ↔ 𝐵 ≠ ∅)) |
18 | 14, 17 | mpbid 222 |
. . . . 5
⊢ (𝜑 → 𝐵 ≠ ∅) |
19 | | n0 3931 |
. . . . 5
⊢ (𝐵 ≠ ∅ ↔
∃𝑎 𝑎 ∈ 𝐵) |
20 | 18, 19 | sylib 208 |
. . . 4
⊢ (𝜑 → ∃𝑎 𝑎 ∈ 𝐵) |
21 | 1 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 𝐵 ∈ 𝑆) |
22 | | simplr 792 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐻) → 𝑎 ∈ 𝐵) |
23 | | oveq2 6658 |
. . . . . . . . . . . 12
⊢ (𝑧 = 𝑎 → (𝑏 + 𝑧) = (𝑏 + 𝑎)) |
24 | | eqid 2622 |
. . . . . . . . . . . 12
⊢ (𝑧 ∈ 𝐵 ↦ (𝑏 + 𝑧)) = (𝑧 ∈ 𝐵 ↦ (𝑏 + 𝑧)) |
25 | | ovex 6678 |
. . . . . . . . . . . 12
⊢ (𝑏 + 𝑎) ∈ V |
26 | 23, 24, 25 | fvmpt 6282 |
. . . . . . . . . . 11
⊢ (𝑎 ∈ 𝐵 → ((𝑧 ∈ 𝐵 ↦ (𝑏 + 𝑧))‘𝑎) = (𝑏 + 𝑎)) |
27 | 22, 26 | syl 17 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐻) → ((𝑧 ∈ 𝐵 ↦ (𝑏 + 𝑧))‘𝑎) = (𝑏 + 𝑎)) |
28 | | ovex 6678 |
. . . . . . . . . . . 12
⊢ (𝑏 + 𝑧) ∈ V |
29 | 28, 24 | fnmpti 6022 |
. . . . . . . . . . 11
⊢ (𝑧 ∈ 𝐵 ↦ (𝑏 + 𝑧)) Fn 𝐵 |
30 | | fnfvelrn 6356 |
. . . . . . . . . . 11
⊢ (((𝑧 ∈ 𝐵 ↦ (𝑏 + 𝑧)) Fn 𝐵 ∧ 𝑎 ∈ 𝐵) → ((𝑧 ∈ 𝐵 ↦ (𝑏 + 𝑧))‘𝑎) ∈ ran (𝑧 ∈ 𝐵 ↦ (𝑏 + 𝑧))) |
31 | 29, 22, 30 | sylancr 695 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐻) → ((𝑧 ∈ 𝐵 ↦ (𝑏 + 𝑧))‘𝑎) ∈ ran (𝑧 ∈ 𝐵 ↦ (𝑏 + 𝑧))) |
32 | 27, 31 | eqeltrrd 2702 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐻) → (𝑏 + 𝑎) ∈ ran (𝑧 ∈ 𝐵 ↦ (𝑏 + 𝑧))) |
33 | | sylow1lem4.h |
. . . . . . . . . . . 12
⊢ 𝐻 = {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐵) = 𝐵} |
34 | | ssrab2 3687 |
. . . . . . . . . . . 12
⊢ {𝑢 ∈ 𝑋 ∣ (𝑢 ⊕ 𝐵) = 𝐵} ⊆ 𝑋 |
35 | 33, 34 | eqsstri 3635 |
. . . . . . . . . . 11
⊢ 𝐻 ⊆ 𝑋 |
36 | | simpr 477 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐻) → 𝑏 ∈ 𝐻) |
37 | 35, 36 | sseldi 3601 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐻) → 𝑏 ∈ 𝑋) |
38 | 1 | ad2antrr 762 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐻) → 𝐵 ∈ 𝑆) |
39 | | mptexg 6484 |
. . . . . . . . . . 11
⊢ (𝐵 ∈ 𝑆 → (𝑧 ∈ 𝐵 ↦ (𝑏 + 𝑧)) ∈ V) |
40 | | rnexg 7098 |
. . . . . . . . . . 11
⊢ ((𝑧 ∈ 𝐵 ↦ (𝑏 + 𝑧)) ∈ V → ran (𝑧 ∈ 𝐵 ↦ (𝑏 + 𝑧)) ∈ V) |
41 | 38, 39, 40 | 3syl 18 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐻) → ran (𝑧 ∈ 𝐵 ↦ (𝑏 + 𝑧)) ∈ V) |
42 | | simpr 477 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = 𝐵) → 𝑦 = 𝐵) |
43 | | simpl 473 |
. . . . . . . . . . . . . 14
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = 𝐵) → 𝑥 = 𝑏) |
44 | 43 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = 𝐵) → (𝑥 + 𝑧) = (𝑏 + 𝑧)) |
45 | 42, 44 | mpteq12dv 4733 |
. . . . . . . . . . . 12
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = 𝐵) → (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) = (𝑧 ∈ 𝐵 ↦ (𝑏 + 𝑧))) |
46 | 45 | rneqd 5353 |
. . . . . . . . . . 11
⊢ ((𝑥 = 𝑏 ∧ 𝑦 = 𝐵) → ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧)) = ran (𝑧 ∈ 𝐵 ↦ (𝑏 + 𝑧))) |
47 | | sylow1lem.m |
. . . . . . . . . . 11
⊢ ⊕ =
(𝑥 ∈ 𝑋, 𝑦 ∈ 𝑆 ↦ ran (𝑧 ∈ 𝑦 ↦ (𝑥 + 𝑧))) |
48 | 46, 47 | ovmpt2ga 6790 |
. . . . . . . . . 10
⊢ ((𝑏 ∈ 𝑋 ∧ 𝐵 ∈ 𝑆 ∧ ran (𝑧 ∈ 𝐵 ↦ (𝑏 + 𝑧)) ∈ V) → (𝑏 ⊕ 𝐵) = ran (𝑧 ∈ 𝐵 ↦ (𝑏 + 𝑧))) |
49 | 37, 38, 41, 48 | syl3anc 1326 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐻) → (𝑏 ⊕ 𝐵) = ran (𝑧 ∈ 𝐵 ↦ (𝑏 + 𝑧))) |
50 | 32, 49 | eleqtrrd 2704 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐻) → (𝑏 + 𝑎) ∈ (𝑏 ⊕ 𝐵)) |
51 | | oveq1 6657 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑏 → (𝑢 ⊕ 𝐵) = (𝑏 ⊕ 𝐵)) |
52 | 51 | eqeq1d 2624 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑏 → ((𝑢 ⊕ 𝐵) = 𝐵 ↔ (𝑏 ⊕ 𝐵) = 𝐵)) |
53 | 52, 33 | elrab2 3366 |
. . . . . . . . . 10
⊢ (𝑏 ∈ 𝐻 ↔ (𝑏 ∈ 𝑋 ∧ (𝑏 ⊕ 𝐵) = 𝐵)) |
54 | 53 | simprbi 480 |
. . . . . . . . 9
⊢ (𝑏 ∈ 𝐻 → (𝑏 ⊕ 𝐵) = 𝐵) |
55 | 54 | adantl 482 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐻) → (𝑏 ⊕ 𝐵) = 𝐵) |
56 | 50, 55 | eleqtrd 2703 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ 𝑏 ∈ 𝐻) → (𝑏 + 𝑎) ∈ 𝐵) |
57 | 56 | ex 450 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (𝑏 ∈ 𝐻 → (𝑏 + 𝑎) ∈ 𝐵)) |
58 | | sylow1.g |
. . . . . . . . 9
⊢ (𝜑 → 𝐺 ∈ Grp) |
59 | 58 | ad2antrr 762 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐻 ∧ 𝑐 ∈ 𝐻)) → 𝐺 ∈ Grp) |
60 | | simprl 794 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐻 ∧ 𝑐 ∈ 𝐻)) → 𝑏 ∈ 𝐻) |
61 | 35, 60 | sseldi 3601 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐻 ∧ 𝑐 ∈ 𝐻)) → 𝑏 ∈ 𝑋) |
62 | | simprr 796 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐻 ∧ 𝑐 ∈ 𝐻)) → 𝑐 ∈ 𝐻) |
63 | 35, 62 | sseldi 3601 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐻 ∧ 𝑐 ∈ 𝐻)) → 𝑐 ∈ 𝑋) |
64 | 6 | simpld 475 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐵 ∈ 𝒫 𝑋) |
65 | 64 | elpwid 4170 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐵 ⊆ 𝑋) |
66 | 65 | sselda 3603 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 𝑎 ∈ 𝑋) |
67 | 66 | adantr 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐻 ∧ 𝑐 ∈ 𝐻)) → 𝑎 ∈ 𝑋) |
68 | | sylow1.x |
. . . . . . . . 9
⊢ 𝑋 = (Base‘𝐺) |
69 | | sylow1lem.a |
. . . . . . . . 9
⊢ + =
(+g‘𝐺) |
70 | 68, 69 | grprcan 17455 |
. . . . . . . 8
⊢ ((𝐺 ∈ Grp ∧ (𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋)) → ((𝑏 + 𝑎) = (𝑐 + 𝑎) ↔ 𝑏 = 𝑐)) |
71 | 59, 61, 63, 67, 70 | syl13anc 1328 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑎 ∈ 𝐵) ∧ (𝑏 ∈ 𝐻 ∧ 𝑐 ∈ 𝐻)) → ((𝑏 + 𝑎) = (𝑐 + 𝑎) ↔ 𝑏 = 𝑐)) |
72 | 71 | ex 450 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → ((𝑏 ∈ 𝐻 ∧ 𝑐 ∈ 𝐻) → ((𝑏 + 𝑎) = (𝑐 + 𝑎) ↔ 𝑏 = 𝑐))) |
73 | 57, 72 | dom2d 7996 |
. . . . 5
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → (𝐵 ∈ 𝑆 → 𝐻 ≼ 𝐵)) |
74 | 21, 73 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ 𝑎 ∈ 𝐵) → 𝐻 ≼ 𝐵) |
75 | 20, 74 | exlimddv 1863 |
. . 3
⊢ (𝜑 → 𝐻 ≼ 𝐵) |
76 | | sylow1.f |
. . . . 5
⊢ (𝜑 → 𝑋 ∈ Fin) |
77 | | ssfi 8180 |
. . . . 5
⊢ ((𝑋 ∈ Fin ∧ 𝐻 ⊆ 𝑋) → 𝐻 ∈ Fin) |
78 | 76, 35, 77 | sylancl 694 |
. . . 4
⊢ (𝜑 → 𝐻 ∈ Fin) |
79 | | ssfi 8180 |
. . . . 5
⊢ ((𝑋 ∈ Fin ∧ 𝐵 ⊆ 𝑋) → 𝐵 ∈ Fin) |
80 | 76, 65, 79 | syl2anc 693 |
. . . 4
⊢ (𝜑 → 𝐵 ∈ Fin) |
81 | | hashdom 13168 |
. . . 4
⊢ ((𝐻 ∈ Fin ∧ 𝐵 ∈ Fin) →
((#‘𝐻) ≤
(#‘𝐵) ↔ 𝐻 ≼ 𝐵)) |
82 | 78, 80, 81 | syl2anc 693 |
. . 3
⊢ (𝜑 → ((#‘𝐻) ≤ (#‘𝐵) ↔ 𝐻 ≼ 𝐵)) |
83 | 75, 82 | mpbird 247 |
. 2
⊢ (𝜑 → (#‘𝐻) ≤ (#‘𝐵)) |
84 | 83, 7 | breqtrd 4679 |
1
⊢ (𝜑 → (#‘𝐻) ≤ (𝑃↑𝑁)) |