Step | Hyp | Ref
| Expression |
1 | | ovex 7328 |
. . 3
⊢
(1...𝑊) ∈
V |
2 | | 2nn0 12278 |
. . . 4
⊢ 2 ∈
ℕ0 |
3 | | vdwlem7.k |
. . . 4
⊢ (𝜑 → 𝐾 ∈
(ℤ≥‘2)) |
4 | | eluznn0 12685 |
. . . 4
⊢ ((2
∈ ℕ0 ∧ 𝐾 ∈ (ℤ≥‘2))
→ 𝐾 ∈
ℕ0) |
5 | 2, 3, 4 | sylancr 586 |
. . 3
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
6 | | vdwlem7.g |
. . 3
⊢ (𝜑 → 𝐺:(1...𝑊)⟶𝑅) |
7 | | vdwlem7.m |
. . 3
⊢ (𝜑 → 𝑀 ∈ ℕ) |
8 | | eqid 2733 |
. . 3
⊢
(1...𝑀) = (1...𝑀) |
9 | 1, 5, 6, 7, 8 | vdwpc 16709 |
. 2
⊢ (𝜑 → (〈𝑀, 𝐾〉 PolyAP 𝐺 ↔ ∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑m
(1...𝑀))(∀𝑖 ∈ (1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀))) |
10 | | vdwlem3.v |
. . . . . 6
⊢ (𝜑 → 𝑉 ∈ ℕ) |
11 | 10 | ad2antrr 722 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ (ℕ ↑m
(1...𝑀)))) ∧
(∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀)) → 𝑉 ∈ ℕ) |
12 | | vdwlem3.w |
. . . . . 6
⊢ (𝜑 → 𝑊 ∈ ℕ) |
13 | 12 | ad2antrr 722 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ (ℕ ↑m
(1...𝑀)))) ∧
(∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀)) → 𝑊 ∈ ℕ) |
14 | | vdwlem4.r |
. . . . . 6
⊢ (𝜑 → 𝑅 ∈ Fin) |
15 | 14 | ad2antrr 722 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ (ℕ ↑m
(1...𝑀)))) ∧
(∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀)) → 𝑅 ∈ Fin) |
16 | | vdwlem4.h |
. . . . . 6
⊢ (𝜑 → 𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅) |
17 | 16 | ad2antrr 722 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ (ℕ ↑m
(1...𝑀)))) ∧
(∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀)) → 𝐻:(1...(𝑊 · (2 · 𝑉)))⟶𝑅) |
18 | | vdwlem4.f |
. . . . 5
⊢ 𝐹 = (𝑥 ∈ (1...𝑉) ↦ (𝑦 ∈ (1...𝑊) ↦ (𝐻‘(𝑦 + (𝑊 · ((𝑥 − 1) + 𝑉)))))) |
19 | 7 | ad2antrr 722 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ (ℕ ↑m
(1...𝑀)))) ∧
(∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀)) → 𝑀 ∈ ℕ) |
20 | 6 | ad2antrr 722 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ (ℕ ↑m
(1...𝑀)))) ∧
(∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀)) → 𝐺:(1...𝑊)⟶𝑅) |
21 | 3 | ad2antrr 722 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ (ℕ ↑m
(1...𝑀)))) ∧
(∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀)) → 𝐾 ∈
(ℤ≥‘2)) |
22 | | vdwlem7.a |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℕ) |
23 | 22 | ad2antrr 722 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ (ℕ ↑m
(1...𝑀)))) ∧
(∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀)) → 𝐴 ∈ ℕ) |
24 | | vdwlem7.d |
. . . . . 6
⊢ (𝜑 → 𝐷 ∈ ℕ) |
25 | 24 | ad2antrr 722 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ (ℕ ↑m
(1...𝑀)))) ∧
(∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀)) → 𝐷 ∈ ℕ) |
26 | | vdwlem7.s |
. . . . . 6
⊢ (𝜑 → (𝐴(AP‘𝐾)𝐷) ⊆ (◡𝐹 “ {𝐺})) |
27 | 26 | ad2antrr 722 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ (ℕ ↑m
(1...𝑀)))) ∧
(∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀)) → (𝐴(AP‘𝐾)𝐷) ⊆ (◡𝐹 “ {𝐺})) |
28 | | simplrl 773 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ (ℕ ↑m
(1...𝑀)))) ∧
(∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀)) → 𝑎 ∈ ℕ) |
29 | | simplrr 774 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ (ℕ ↑m
(1...𝑀)))) ∧
(∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀)) → 𝑑 ∈ (ℕ ↑m
(1...𝑀))) |
30 | | nnex 12007 |
. . . . . . 7
⊢ ℕ
∈ V |
31 | | ovex 7328 |
. . . . . . 7
⊢
(1...𝑀) ∈
V |
32 | 30, 31 | elmap 8679 |
. . . . . 6
⊢ (𝑑 ∈ (ℕ
↑m (1...𝑀))
↔ 𝑑:(1...𝑀)⟶ℕ) |
33 | 29, 32 | sylib 217 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ (ℕ ↑m
(1...𝑀)))) ∧
(∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀)) → 𝑑:(1...𝑀)⟶ℕ) |
34 | | simprl 767 |
. . . . . 6
⊢ (((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ (ℕ ↑m
(1...𝑀)))) ∧
(∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀)) → ∀𝑖 ∈ (1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))})) |
35 | | fveq2 6792 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑘 → (𝑑‘𝑖) = (𝑑‘𝑘)) |
36 | 35 | oveq2d 7311 |
. . . . . . . . 9
⊢ (𝑖 = 𝑘 → (𝑎 + (𝑑‘𝑖)) = (𝑎 + (𝑑‘𝑘))) |
37 | 36, 35 | oveq12d 7313 |
. . . . . . . 8
⊢ (𝑖 = 𝑘 → ((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) = ((𝑎 + (𝑑‘𝑘))(AP‘𝐾)(𝑑‘𝑘))) |
38 | 36 | fveq2d 6796 |
. . . . . . . . . 10
⊢ (𝑖 = 𝑘 → (𝐺‘(𝑎 + (𝑑‘𝑖))) = (𝐺‘(𝑎 + (𝑑‘𝑘)))) |
39 | 38 | sneqd 4576 |
. . . . . . . . 9
⊢ (𝑖 = 𝑘 → {(𝐺‘(𝑎 + (𝑑‘𝑖)))} = {(𝐺‘(𝑎 + (𝑑‘𝑘)))}) |
40 | 39 | imaeq2d 5970 |
. . . . . . . 8
⊢ (𝑖 = 𝑘 → (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) = (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑘)))})) |
41 | 37, 40 | sseq12d 3956 |
. . . . . . 7
⊢ (𝑖 = 𝑘 → (((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ↔ ((𝑎 + (𝑑‘𝑘))(AP‘𝐾)(𝑑‘𝑘)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑘)))}))) |
42 | 41 | cbvralvw 3385 |
. . . . . 6
⊢
(∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ↔ ∀𝑘 ∈ (1...𝑀)((𝑎 + (𝑑‘𝑘))(AP‘𝐾)(𝑑‘𝑘)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑘)))})) |
43 | 34, 42 | sylib 217 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ (ℕ ↑m
(1...𝑀)))) ∧
(∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀)) → ∀𝑘 ∈ (1...𝑀)((𝑎 + (𝑑‘𝑘))(AP‘𝐾)(𝑑‘𝑘)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑘)))})) |
44 | 38 | cbvmptv 5190 |
. . . . 5
⊢ (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖)))) = (𝑘 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑘)))) |
45 | | simprr 769 |
. . . . 5
⊢ (((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ (ℕ ↑m
(1...𝑀)))) ∧
(∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀)) → (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀) |
46 | | eqid 2733 |
. . . . 5
⊢ (𝑎 + (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1))) = (𝑎 + (𝑊 · ((𝐴 + (𝑉 − 𝐷)) − 1))) |
47 | | eqid 2733 |
. . . . 5
⊢ (𝑗 ∈ (1...(𝑀 + 1)) ↦ (if(𝑗 = (𝑀 + 1), 0, (𝑑‘𝑗)) + (𝑊 · 𝐷))) = (𝑗 ∈ (1...(𝑀 + 1)) ↦ (if(𝑗 = (𝑀 + 1), 0, (𝑑‘𝑗)) + (𝑊 · 𝐷))) |
48 | 11, 13, 15, 17, 18, 19, 20, 21, 23, 25, 27, 28, 33, 43, 44, 45, 46, 47 | vdwlem6 16715 |
. . . 4
⊢ (((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ (ℕ ↑m
(1...𝑀)))) ∧
(∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀)) → (〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐺)) |
49 | 48 | ex 412 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ ℕ ∧ 𝑑 ∈ (ℕ ↑m
(1...𝑀)))) →
((∀𝑖 ∈
(1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀) → (〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐺))) |
50 | 49 | rexlimdvva 3199 |
. 2
⊢ (𝜑 → (∃𝑎 ∈ ℕ ∃𝑑 ∈ (ℕ ↑m
(1...𝑀))(∀𝑖 ∈ (1...𝑀)((𝑎 + (𝑑‘𝑖))(AP‘𝐾)(𝑑‘𝑖)) ⊆ (◡𝐺 “ {(𝐺‘(𝑎 + (𝑑‘𝑖)))}) ∧ (♯‘ran (𝑖 ∈ (1...𝑀) ↦ (𝐺‘(𝑎 + (𝑑‘𝑖))))) = 𝑀) → (〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐺))) |
51 | 9, 50 | sylbid 239 |
1
⊢ (𝜑 → (〈𝑀, 𝐾〉 PolyAP 𝐺 → (〈(𝑀 + 1), 𝐾〉 PolyAP 𝐻 ∨ (𝐾 + 1) MonoAP 𝐺))) |