Step | Hyp | Ref
| Expression |
1 | | sylow2a.y |
. . . . 5
⊢ (𝜑 → 𝑌 ∈ Fin) |
2 | | pwfi 8949 |
. . . . 5
⊢ (𝑌 ∈ Fin ↔ 𝒫
𝑌 ∈
Fin) |
3 | 1, 2 | sylib 217 |
. . . 4
⊢ (𝜑 → 𝒫 𝑌 ∈ Fin) |
4 | | sylow2a.m |
. . . . . 6
⊢ (𝜑 → ⊕ ∈ (𝐺 GrpAct 𝑌)) |
5 | | sylow2a.r |
. . . . . . 7
⊢ ∼ =
{〈𝑥, 𝑦〉 ∣ ({𝑥, 𝑦} ⊆ 𝑌 ∧ ∃𝑔 ∈ 𝑋 (𝑔 ⊕ 𝑥) = 𝑦)} |
6 | | sylow2a.x |
. . . . . . 7
⊢ 𝑋 = (Base‘𝐺) |
7 | 5, 6 | gaorber 18902 |
. . . . . 6
⊢ ( ⊕ ∈
(𝐺 GrpAct 𝑌) → ∼ Er 𝑌) |
8 | 4, 7 | syl 17 |
. . . . 5
⊢ (𝜑 → ∼ Er 𝑌) |
9 | 8 | qsss 8555 |
. . . 4
⊢ (𝜑 → (𝑌 / ∼ ) ⊆ 𝒫
𝑌) |
10 | 3, 9 | ssfid 9030 |
. . 3
⊢ (𝜑 → (𝑌 / ∼ ) ∈
Fin) |
11 | | diffi 8950 |
. . 3
⊢ ((𝑌 / ∼ ) ∈ Fin →
((𝑌 / ∼ )
∖ 𝒫 𝑍) ∈
Fin) |
12 | 10, 11 | syl 17 |
. 2
⊢ (𝜑 → ((𝑌 / ∼ ) ∖ 𝒫
𝑍) ∈
Fin) |
13 | | sylow2a.p |
. . . . 5
⊢ (𝜑 → 𝑃 pGrp 𝐺) |
14 | | gagrp 18886 |
. . . . . . 7
⊢ ( ⊕ ∈
(𝐺 GrpAct 𝑌) → 𝐺 ∈ Grp) |
15 | 4, 14 | syl 17 |
. . . . . 6
⊢ (𝜑 → 𝐺 ∈ Grp) |
16 | | sylow2a.f |
. . . . . 6
⊢ (𝜑 → 𝑋 ∈ Fin) |
17 | 6 | pgpfi 19198 |
. . . . . 6
⊢ ((𝐺 ∈ Grp ∧ 𝑋 ∈ Fin) → (𝑃 pGrp 𝐺 ↔ (𝑃 ∈ ℙ ∧ ∃𝑛 ∈ ℕ0
(♯‘𝑋) = (𝑃↑𝑛)))) |
18 | 15, 16, 17 | syl2anc 584 |
. . . . 5
⊢ (𝜑 → (𝑃 pGrp 𝐺 ↔ (𝑃 ∈ ℙ ∧ ∃𝑛 ∈ ℕ0
(♯‘𝑋) = (𝑃↑𝑛)))) |
19 | 13, 18 | mpbid 231 |
. . . 4
⊢ (𝜑 → (𝑃 ∈ ℙ ∧ ∃𝑛 ∈ ℕ0
(♯‘𝑋) = (𝑃↑𝑛))) |
20 | 19 | simpld 495 |
. . 3
⊢ (𝜑 → 𝑃 ∈ ℙ) |
21 | | prmz 16368 |
. . 3
⊢ (𝑃 ∈ ℙ → 𝑃 ∈
ℤ) |
22 | 20, 21 | syl 17 |
. 2
⊢ (𝜑 → 𝑃 ∈ ℤ) |
23 | | eldifi 4061 |
. . . . 5
⊢ (𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫
𝑍) → 𝑧 ∈ (𝑌 / ∼ )) |
24 | 1 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → 𝑌 ∈ Fin) |
25 | 9 | sselda 3921 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → 𝑧 ∈ 𝒫 𝑌) |
26 | 25 | elpwid 4545 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → 𝑧 ⊆ 𝑌) |
27 | 24, 26 | ssfid 9030 |
. . . . 5
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → 𝑧 ∈ Fin) |
28 | 23, 27 | sylan2 593 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫
𝑍)) → 𝑧 ∈ Fin) |
29 | | hashcl 14059 |
. . . 4
⊢ (𝑧 ∈ Fin →
(♯‘𝑧) ∈
ℕ0) |
30 | 28, 29 | syl 17 |
. . 3
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫
𝑍)) →
(♯‘𝑧) ∈
ℕ0) |
31 | 30 | nn0zd 12412 |
. 2
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫
𝑍)) →
(♯‘𝑧) ∈
ℤ) |
32 | | eldif 3897 |
. . 3
⊢ (𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫
𝑍) ↔ (𝑧 ∈ (𝑌 / ∼ ) ∧ ¬ 𝑧 ∈ 𝒫 𝑍)) |
33 | | eqid 2738 |
. . . . 5
⊢ (𝑌 / ∼ ) = (𝑌 / ∼ ) |
34 | | sseq1 3946 |
. . . . . . . 8
⊢ ([𝑤] ∼ = 𝑧 → ([𝑤] ∼ ⊆ 𝑍 ↔ 𝑧 ⊆ 𝑍)) |
35 | | velpw 4539 |
. . . . . . . 8
⊢ (𝑧 ∈ 𝒫 𝑍 ↔ 𝑧 ⊆ 𝑍) |
36 | 34, 35 | bitr4di 289 |
. . . . . . 7
⊢ ([𝑤] ∼ = 𝑧 → ([𝑤] ∼ ⊆ 𝑍 ↔ 𝑧 ∈ 𝒫 𝑍)) |
37 | 36 | notbid 318 |
. . . . . 6
⊢ ([𝑤] ∼ = 𝑧 → (¬ [𝑤] ∼ ⊆ 𝑍 ↔ ¬ 𝑧 ∈ 𝒫 𝑍)) |
38 | | fveq2 6767 |
. . . . . . 7
⊢ ([𝑤] ∼ = 𝑧 → (♯‘[𝑤] ∼ ) =
(♯‘𝑧)) |
39 | 38 | breq2d 5086 |
. . . . . 6
⊢ ([𝑤] ∼ = 𝑧 → (𝑃 ∥ (♯‘[𝑤] ∼ ) ↔ 𝑃 ∥ (♯‘𝑧))) |
40 | 37, 39 | imbi12d 345 |
. . . . 5
⊢ ([𝑤] ∼ = 𝑧 → ((¬ [𝑤] ∼ ⊆ 𝑍 → 𝑃 ∥ (♯‘[𝑤] ∼ )) ↔ (¬
𝑧 ∈ 𝒫 𝑍 → 𝑃 ∥ (♯‘𝑧)))) |
41 | 20 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → 𝑃 ∈ ℙ) |
42 | 8 | adantr 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ∼ Er 𝑌) |
43 | | simpr 485 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → 𝑤 ∈ 𝑌) |
44 | 42, 43 | erref 8506 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → 𝑤 ∼ 𝑤) |
45 | | vex 3434 |
. . . . . . . . . . . . . 14
⊢ 𝑤 ∈ V |
46 | 45, 45 | elec 8530 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ [𝑤] ∼ ↔ 𝑤 ∼ 𝑤) |
47 | 44, 46 | sylibr 233 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → 𝑤 ∈ [𝑤] ∼ ) |
48 | 47 | ne0d 4270 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → [𝑤] ∼ ≠
∅) |
49 | 8 | ecss 8532 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → [𝑤] ∼ ⊆ 𝑌) |
50 | 1, 49 | ssfid 9030 |
. . . . . . . . . . . . 13
⊢ (𝜑 → [𝑤] ∼ ∈
Fin) |
51 | 50 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → [𝑤] ∼ ∈
Fin) |
52 | | hashnncl 14069 |
. . . . . . . . . . . 12
⊢ ([𝑤] ∼ ∈ Fin →
((♯‘[𝑤] ∼ )
∈ ℕ ↔ [𝑤]
∼
≠ ∅)) |
53 | 51, 52 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ((♯‘[𝑤] ∼ ) ∈ ℕ
↔ [𝑤] ∼ ≠
∅)) |
54 | 48, 53 | mpbird 256 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (♯‘[𝑤] ∼ ) ∈
ℕ) |
55 | | pceq0 16560 |
. . . . . . . . . 10
⊢ ((𝑃 ∈ ℙ ∧
(♯‘[𝑤] ∼ )
∈ ℕ) → ((𝑃
pCnt (♯‘[𝑤]
∼
)) = 0 ↔ ¬ 𝑃
∥ (♯‘[𝑤]
∼
))) |
56 | 41, 54, 55 | syl2anc 584 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ((𝑃 pCnt (♯‘[𝑤] ∼ )) = 0 ↔ ¬
𝑃 ∥
(♯‘[𝑤] ∼
))) |
57 | | oveq2 7276 |
. . . . . . . . . 10
⊢ ((𝑃 pCnt (♯‘[𝑤] ∼ )) = 0 →
(𝑃↑(𝑃 pCnt (♯‘[𝑤] ∼ ))) = (𝑃↑0)) |
58 | | hashcl 14059 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ([𝑤] ∼ ∈ Fin →
(♯‘[𝑤] ∼ )
∈ ℕ0) |
59 | 50, 58 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (♯‘[𝑤] ∼ ) ∈
ℕ0) |
60 | 59 | nn0zd 12412 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (♯‘[𝑤] ∼ ) ∈
ℤ) |
61 | | ssrab2 4013 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ {𝑣 ∈ 𝑋 ∣ (𝑣 ⊕ 𝑤) = 𝑤} ⊆ 𝑋 |
62 | | ssfi 8944 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑋 ∈ Fin ∧ {𝑣 ∈ 𝑋 ∣ (𝑣 ⊕ 𝑤) = 𝑤} ⊆ 𝑋) → {𝑣 ∈ 𝑋 ∣ (𝑣 ⊕ 𝑤) = 𝑤} ∈ Fin) |
63 | 16, 61, 62 | sylancl 586 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → {𝑣 ∈ 𝑋 ∣ (𝑣 ⊕ 𝑤) = 𝑤} ∈ Fin) |
64 | | hashcl 14059 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ({𝑣 ∈ 𝑋 ∣ (𝑣 ⊕ 𝑤) = 𝑤} ∈ Fin → (♯‘{𝑣 ∈ 𝑋 ∣ (𝑣 ⊕ 𝑤) = 𝑤}) ∈
ℕ0) |
65 | 63, 64 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → (♯‘{𝑣 ∈ 𝑋 ∣ (𝑣 ⊕ 𝑤) = 𝑤}) ∈
ℕ0) |
66 | 65 | nn0zd 12412 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → (♯‘{𝑣 ∈ 𝑋 ∣ (𝑣 ⊕ 𝑤) = 𝑤}) ∈ ℤ) |
67 | | dvdsmul1 15975 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((♯‘[𝑤]
∼
) ∈ ℤ ∧ (♯‘{𝑣 ∈ 𝑋 ∣ (𝑣 ⊕ 𝑤) = 𝑤}) ∈ ℤ) →
(♯‘[𝑤] ∼ )
∥ ((♯‘[𝑤]
∼
) · (♯‘{𝑣 ∈ 𝑋 ∣ (𝑣 ⊕ 𝑤) = 𝑤}))) |
68 | 60, 66, 67 | syl2anc 584 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝜑 → (♯‘[𝑤] ∼ ) ∥
((♯‘[𝑤] ∼ )
· (♯‘{𝑣
∈ 𝑋 ∣ (𝑣 ⊕ 𝑤) = 𝑤}))) |
69 | 68 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (♯‘[𝑤] ∼ ) ∥
((♯‘[𝑤] ∼ )
· (♯‘{𝑣
∈ 𝑋 ∣ (𝑣 ⊕ 𝑤) = 𝑤}))) |
70 | 4 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ⊕ ∈ (𝐺 GrpAct 𝑌)) |
71 | 16 | adantr 481 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → 𝑋 ∈ Fin) |
72 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . 20
⊢ {𝑣 ∈ 𝑋 ∣ (𝑣 ⊕ 𝑤) = 𝑤} = {𝑣 ∈ 𝑋 ∣ (𝑣 ⊕ 𝑤) = 𝑤} |
73 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝐺 ~QG {𝑣 ∈ 𝑋 ∣ (𝑣 ⊕ 𝑤) = 𝑤}) = (𝐺 ~QG {𝑣 ∈ 𝑋 ∣ (𝑣 ⊕ 𝑤) = 𝑤}) |
74 | 6, 72, 73, 5 | orbsta2 18908 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((( ⊕ ∈
(𝐺 GrpAct 𝑌) ∧ 𝑤 ∈ 𝑌) ∧ 𝑋 ∈ Fin) → (♯‘𝑋) = ((♯‘[𝑤] ∼ ) ·
(♯‘{𝑣 ∈
𝑋 ∣ (𝑣 ⊕ 𝑤) = 𝑤}))) |
75 | 70, 43, 71, 74 | syl21anc 835 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (♯‘𝑋) = ((♯‘[𝑤] ∼ ) ·
(♯‘{𝑣 ∈
𝑋 ∣ (𝑣 ⊕ 𝑤) = 𝑤}))) |
76 | 69, 75 | breqtrrd 5102 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (♯‘[𝑤] ∼ ) ∥
(♯‘𝑋)) |
77 | 19 | simprd 496 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∃𝑛 ∈ ℕ0
(♯‘𝑋) = (𝑃↑𝑛)) |
78 | 77 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ∃𝑛 ∈ ℕ0
(♯‘𝑋) = (𝑃↑𝑛)) |
79 | | breq2 5078 |
. . . . . . . . . . . . . . . . . . 19
⊢
((♯‘𝑋) =
(𝑃↑𝑛) → ((♯‘[𝑤] ∼ ) ∥
(♯‘𝑋) ↔
(♯‘[𝑤] ∼ )
∥ (𝑃↑𝑛))) |
80 | 79 | biimpcd 248 |
. . . . . . . . . . . . . . . . . 18
⊢
((♯‘[𝑤]
∼
) ∥ (♯‘𝑋)
→ ((♯‘𝑋) =
(𝑃↑𝑛) → (♯‘[𝑤] ∼ ) ∥ (𝑃↑𝑛))) |
81 | 80 | reximdv 3200 |
. . . . . . . . . . . . . . . . 17
⊢
((♯‘[𝑤]
∼
) ∥ (♯‘𝑋)
→ (∃𝑛 ∈
ℕ0 (♯‘𝑋) = (𝑃↑𝑛) → ∃𝑛 ∈ ℕ0
(♯‘[𝑤] ∼ )
∥ (𝑃↑𝑛))) |
82 | 76, 78, 81 | sylc 65 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ∃𝑛 ∈ ℕ0
(♯‘[𝑤] ∼ )
∥ (𝑃↑𝑛)) |
83 | | pcprmpw2 16571 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑃 ∈ ℙ ∧
(♯‘[𝑤] ∼ )
∈ ℕ) → (∃𝑛 ∈ ℕ0
(♯‘[𝑤] ∼ )
∥ (𝑃↑𝑛) ↔ (♯‘[𝑤] ∼ ) = (𝑃↑(𝑃 pCnt (♯‘[𝑤] ∼
))))) |
84 | 41, 54, 83 | syl2anc 584 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (∃𝑛 ∈ ℕ0
(♯‘[𝑤] ∼ )
∥ (𝑃↑𝑛) ↔ (♯‘[𝑤] ∼ ) = (𝑃↑(𝑃 pCnt (♯‘[𝑤] ∼
))))) |
85 | 82, 84 | mpbid 231 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (♯‘[𝑤] ∼ ) = (𝑃↑(𝑃 pCnt (♯‘[𝑤] ∼
)))) |
86 | 85 | eqcomd 2744 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (𝑃↑(𝑃 pCnt (♯‘[𝑤] ∼ ))) =
(♯‘[𝑤] ∼
)) |
87 | 22 | adantr 481 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → 𝑃 ∈ ℤ) |
88 | 87 | zcnd 12415 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → 𝑃 ∈ ℂ) |
89 | 88 | exp0d 13846 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (𝑃↑0) = 1) |
90 | | hash1 14107 |
. . . . . . . . . . . . . . 15
⊢
(♯‘1o) = 1 |
91 | 89, 90 | eqtr4di 2796 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (𝑃↑0) =
(♯‘1o)) |
92 | 86, 91 | eqeq12d 2754 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ((𝑃↑(𝑃 pCnt (♯‘[𝑤] ∼ ))) = (𝑃↑0) ↔
(♯‘[𝑤] ∼ ) =
(♯‘1o))) |
93 | | df1o2 8292 |
. . . . . . . . . . . . . . 15
⊢
1o = {∅} |
94 | | snfi 8822 |
. . . . . . . . . . . . . . 15
⊢ {∅}
∈ Fin |
95 | 93, 94 | eqeltri 2835 |
. . . . . . . . . . . . . 14
⊢
1o ∈ Fin |
96 | | hashen 14049 |
. . . . . . . . . . . . . 14
⊢ (([𝑤] ∼ ∈ Fin ∧
1o ∈ Fin) → ((♯‘[𝑤] ∼ ) =
(♯‘1o) ↔ [𝑤] ∼ ≈
1o)) |
97 | 51, 95, 96 | sylancl 586 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ((♯‘[𝑤] ∼ ) =
(♯‘1o) ↔ [𝑤] ∼ ≈
1o)) |
98 | 92, 97 | bitrd 278 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ((𝑃↑(𝑃 pCnt (♯‘[𝑤] ∼ ))) = (𝑃↑0) ↔ [𝑤] ∼ ≈
1o)) |
99 | | en1b 8801 |
. . . . . . . . . . . 12
⊢ ([𝑤] ∼ ≈
1o ↔ [𝑤]
∼
= {∪ [𝑤] ∼ }) |
100 | 98, 99 | bitrdi 287 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ((𝑃↑(𝑃 pCnt (♯‘[𝑤] ∼ ))) = (𝑃↑0) ↔ [𝑤] ∼ = {∪ [𝑤]
∼
})) |
101 | 43 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑌) ∧ (ℎ ∈ 𝑋 ∧ [𝑤] ∼ = {∪ [𝑤]
∼
})) → 𝑤 ∈ 𝑌) |
102 | 4 | ad2antrr 723 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑌) ∧ (ℎ ∈ 𝑋 ∧ [𝑤] ∼ = {∪ [𝑤]
∼
})) → ⊕ ∈ (𝐺 GrpAct 𝑌)) |
103 | 6 | gaf 18889 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ( ⊕ ∈
(𝐺 GrpAct 𝑌) → ⊕ :(𝑋 × 𝑌)⟶𝑌) |
104 | 102, 103 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑌) ∧ (ℎ ∈ 𝑋 ∧ [𝑤] ∼ = {∪ [𝑤]
∼
})) → ⊕ :(𝑋 × 𝑌)⟶𝑌) |
105 | | simprl 768 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑌) ∧ (ℎ ∈ 𝑋 ∧ [𝑤] ∼ = {∪ [𝑤]
∼
})) → ℎ ∈ 𝑋) |
106 | 104, 105,
101 | fovrnd 7435 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑌) ∧ (ℎ ∈ 𝑋 ∧ [𝑤] ∼ = {∪ [𝑤]
∼
})) → (ℎ ⊕ 𝑤) ∈ 𝑌) |
107 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . 19
⊢ (ℎ ⊕ 𝑤) = (ℎ ⊕ 𝑤) |
108 | | oveq1 7275 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = ℎ → (𝑘 ⊕ 𝑤) = (ℎ ⊕ 𝑤)) |
109 | 108 | eqeq1d 2740 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = ℎ → ((𝑘 ⊕ 𝑤) = (ℎ ⊕ 𝑤) ↔ (ℎ ⊕ 𝑤) = (ℎ ⊕ 𝑤))) |
110 | 109 | rspcev 3560 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((ℎ ∈ 𝑋 ∧ (ℎ ⊕ 𝑤) = (ℎ ⊕ 𝑤)) → ∃𝑘 ∈ 𝑋 (𝑘 ⊕ 𝑤) = (ℎ ⊕ 𝑤)) |
111 | 105, 107,
110 | sylancl 586 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑌) ∧ (ℎ ∈ 𝑋 ∧ [𝑤] ∼ = {∪ [𝑤]
∼
})) → ∃𝑘 ∈
𝑋 (𝑘 ⊕ 𝑤) = (ℎ ⊕ 𝑤)) |
112 | 5 | gaorb 18901 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑤 ∼ (ℎ ⊕ 𝑤) ↔ (𝑤 ∈ 𝑌 ∧ (ℎ ⊕ 𝑤) ∈ 𝑌 ∧ ∃𝑘 ∈ 𝑋 (𝑘 ⊕ 𝑤) = (ℎ ⊕ 𝑤))) |
113 | 101, 106,
111, 112 | syl3anbrc 1342 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑌) ∧ (ℎ ∈ 𝑋 ∧ [𝑤] ∼ = {∪ [𝑤]
∼
})) → 𝑤 ∼ (ℎ ⊕ 𝑤)) |
114 | | ovex 7301 |
. . . . . . . . . . . . . . . . . 18
⊢ (ℎ ⊕ 𝑤) ∈ V |
115 | 114, 45 | elec 8530 |
. . . . . . . . . . . . . . . . 17
⊢ ((ℎ ⊕ 𝑤) ∈ [𝑤] ∼ ↔ 𝑤 ∼ (ℎ ⊕ 𝑤)) |
116 | 113, 115 | sylibr 233 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑌) ∧ (ℎ ∈ 𝑋 ∧ [𝑤] ∼ = {∪ [𝑤]
∼
})) → (ℎ ⊕ 𝑤) ∈ [𝑤] ∼ ) |
117 | | simprr 770 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑌) ∧ (ℎ ∈ 𝑋 ∧ [𝑤] ∼ = {∪ [𝑤]
∼
})) → [𝑤] ∼ =
{∪ [𝑤] ∼ }) |
118 | 116, 117 | eleqtrd 2841 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑌) ∧ (ℎ ∈ 𝑋 ∧ [𝑤] ∼ = {∪ [𝑤]
∼
})) → (ℎ ⊕ 𝑤) ∈ {∪ [𝑤]
∼
}) |
119 | 114 | elsn 4577 |
. . . . . . . . . . . . . . 15
⊢ ((ℎ ⊕ 𝑤) ∈ {∪ [𝑤] ∼ } ↔ (ℎ ⊕ 𝑤) = ∪ [𝑤] ∼ ) |
120 | 118, 119 | sylib 217 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑌) ∧ (ℎ ∈ 𝑋 ∧ [𝑤] ∼ = {∪ [𝑤]
∼
})) → (ℎ ⊕ 𝑤) = ∪
[𝑤] ∼ ) |
121 | 47 | adantr 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑌) ∧ (ℎ ∈ 𝑋 ∧ [𝑤] ∼ = {∪ [𝑤]
∼
})) → 𝑤 ∈ [𝑤] ∼ ) |
122 | 121, 117 | eleqtrd 2841 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑌) ∧ (ℎ ∈ 𝑋 ∧ [𝑤] ∼ = {∪ [𝑤]
∼
})) → 𝑤 ∈ {∪ [𝑤]
∼
}) |
123 | 45 | elsn 4577 |
. . . . . . . . . . . . . . 15
⊢ (𝑤 ∈ {∪ [𝑤]
∼
} ↔ 𝑤 = ∪ [𝑤]
∼
) |
124 | 122, 123 | sylib 217 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑌) ∧ (ℎ ∈ 𝑋 ∧ [𝑤] ∼ = {∪ [𝑤]
∼
})) → 𝑤 = ∪ [𝑤]
∼
) |
125 | 120, 124 | eqtr4d 2781 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑌) ∧ (ℎ ∈ 𝑋 ∧ [𝑤] ∼ = {∪ [𝑤]
∼
})) → (ℎ ⊕ 𝑤) = 𝑤) |
126 | 125 | expr 457 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑤 ∈ 𝑌) ∧ ℎ ∈ 𝑋) → ([𝑤] ∼ = {∪ [𝑤]
∼
} → (ℎ ⊕ 𝑤) = 𝑤)) |
127 | 126 | ralrimdva 3118 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ([𝑤] ∼ = {∪ [𝑤]
∼
} → ∀ℎ ∈
𝑋 (ℎ ⊕ 𝑤) = 𝑤)) |
128 | 100, 127 | sylbid 239 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ((𝑃↑(𝑃 pCnt (♯‘[𝑤] ∼ ))) = (𝑃↑0) → ∀ℎ ∈ 𝑋 (ℎ ⊕ 𝑤) = 𝑤)) |
129 | 57, 128 | syl5 34 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → ((𝑃 pCnt (♯‘[𝑤] ∼ )) = 0 →
∀ℎ ∈ 𝑋 (ℎ ⊕ 𝑤) = 𝑤)) |
130 | 56, 129 | sylbird 259 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (¬ 𝑃 ∥ (♯‘[𝑤] ∼ ) →
∀ℎ ∈ 𝑋 (ℎ ⊕ 𝑤) = 𝑤)) |
131 | | oveq2 7276 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑤 → (ℎ ⊕ 𝑢) = (ℎ ⊕ 𝑤)) |
132 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑤 → 𝑢 = 𝑤) |
133 | 131, 132 | eqeq12d 2754 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑤 → ((ℎ ⊕ 𝑢) = 𝑢 ↔ (ℎ ⊕ 𝑤) = 𝑤)) |
134 | 133 | ralbidv 3108 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑤 → (∀ℎ ∈ 𝑋 (ℎ ⊕ 𝑢) = 𝑢 ↔ ∀ℎ ∈ 𝑋 (ℎ ⊕ 𝑤) = 𝑤)) |
135 | | sylow2a.z |
. . . . . . . . . . 11
⊢ 𝑍 = {𝑢 ∈ 𝑌 ∣ ∀ℎ ∈ 𝑋 (ℎ ⊕ 𝑢) = 𝑢} |
136 | 134, 135 | elrab2 3627 |
. . . . . . . . . 10
⊢ (𝑤 ∈ 𝑍 ↔ (𝑤 ∈ 𝑌 ∧ ∀ℎ ∈ 𝑋 (ℎ ⊕ 𝑤) = 𝑤)) |
137 | 136 | baib 536 |
. . . . . . . . 9
⊢ (𝑤 ∈ 𝑌 → (𝑤 ∈ 𝑍 ↔ ∀ℎ ∈ 𝑋 (ℎ ⊕ 𝑤) = 𝑤)) |
138 | 137 | adantl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (𝑤 ∈ 𝑍 ↔ ∀ℎ ∈ 𝑋 (ℎ ⊕ 𝑤) = 𝑤)) |
139 | 130, 138 | sylibrd 258 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (¬ 𝑃 ∥ (♯‘[𝑤] ∼ ) → 𝑤 ∈ 𝑍)) |
140 | 6, 4, 13, 16, 1, 135, 5 | sylow2alem1 19210 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → [𝑤] ∼ = {𝑤}) |
141 | | simpr 485 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → 𝑤 ∈ 𝑍) |
142 | 141 | snssd 4743 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → {𝑤} ⊆ 𝑍) |
143 | 140, 142 | eqsstrd 3959 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑍) → [𝑤] ∼ ⊆ 𝑍) |
144 | 143 | ex 413 |
. . . . . . . 8
⊢ (𝜑 → (𝑤 ∈ 𝑍 → [𝑤] ∼ ⊆ 𝑍)) |
145 | 144 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (𝑤 ∈ 𝑍 → [𝑤] ∼ ⊆ 𝑍)) |
146 | 139, 145 | syld 47 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (¬ 𝑃 ∥ (♯‘[𝑤] ∼ ) → [𝑤] ∼ ⊆ 𝑍)) |
147 | 146 | con1d 145 |
. . . . 5
⊢ ((𝜑 ∧ 𝑤 ∈ 𝑌) → (¬ [𝑤] ∼ ⊆ 𝑍 → 𝑃 ∥ (♯‘[𝑤] ∼
))) |
148 | 33, 40, 147 | ectocld 8561 |
. . . 4
⊢ ((𝜑 ∧ 𝑧 ∈ (𝑌 / ∼ )) → (¬
𝑧 ∈ 𝒫 𝑍 → 𝑃 ∥ (♯‘𝑧))) |
149 | 148 | impr 455 |
. . 3
⊢ ((𝜑 ∧ (𝑧 ∈ (𝑌 / ∼ ) ∧ ¬ 𝑧 ∈ 𝒫 𝑍)) → 𝑃 ∥ (♯‘𝑧)) |
150 | 32, 149 | sylan2b 594 |
. 2
⊢ ((𝜑 ∧ 𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫
𝑍)) → 𝑃 ∥ (♯‘𝑧)) |
151 | 12, 22, 31, 150 | fsumdvds 16005 |
1
⊢ (𝜑 → 𝑃 ∥ Σ𝑧 ∈ ((𝑌 / ∼ ) ∖ 𝒫
𝑍)(♯‘𝑧)) |