Step | Hyp | Ref
| Expression |
1 | | plycj.4 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) |
2 | | plycj.1 |
. . . . 5
⊢ 𝑁 = (deg‘𝐹) |
3 | | plycj.2 |
. . . . 5
⊢ 𝐺 = ((∗ ∘ 𝐹) ∘
∗) |
4 | | eqid 2737 |
. . . . 5
⊢
(coeff‘𝐹) =
(coeff‘𝐹) |
5 | 2, 3, 4 | plycjlem 25170 |
. . . 4
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((∗ ∘ (coeff‘𝐹))‘𝑘) · (𝑧↑𝑘)))) |
6 | 1, 5 | syl 17 |
. . 3
⊢ (𝜑 → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((∗ ∘ (coeff‘𝐹))‘𝑘) · (𝑧↑𝑘)))) |
7 | | plybss 25088 |
. . . . . 6
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝑆 ⊆ ℂ) |
8 | 1, 7 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
9 | | 0cnd 10826 |
. . . . . 6
⊢ (𝜑 → 0 ∈
ℂ) |
10 | 9 | snssd 4722 |
. . . . 5
⊢ (𝜑 → {0} ⊆
ℂ) |
11 | 8, 10 | unssd 4100 |
. . . 4
⊢ (𝜑 → (𝑆 ∪ {0}) ⊆
ℂ) |
12 | | dgrcl 25127 |
. . . . . 6
⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) ∈
ℕ0) |
13 | 1, 12 | syl 17 |
. . . . 5
⊢ (𝜑 → (deg‘𝐹) ∈
ℕ0) |
14 | 2, 13 | eqeltrid 2842 |
. . . 4
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
15 | 4 | coef 25124 |
. . . . . . 7
⊢ (𝐹 ∈ (Poly‘𝑆) → (coeff‘𝐹):ℕ0⟶(𝑆 ∪ {0})) |
16 | 1, 15 | syl 17 |
. . . . . 6
⊢ (𝜑 → (coeff‘𝐹):ℕ0⟶(𝑆 ∪ {0})) |
17 | | elfznn0 13205 |
. . . . . 6
⊢ (𝑘 ∈ (0...𝑁) → 𝑘 ∈ ℕ0) |
18 | | fvco3 6810 |
. . . . . 6
⊢
(((coeff‘𝐹):ℕ0⟶(𝑆 ∪ {0}) ∧ 𝑘 ∈ ℕ0)
→ ((∗ ∘ (coeff‘𝐹))‘𝑘) = (∗‘((coeff‘𝐹)‘𝑘))) |
19 | 16, 17, 18 | syl2an 599 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((∗ ∘
(coeff‘𝐹))‘𝑘) = (∗‘((coeff‘𝐹)‘𝑘))) |
20 | | ffvelrn 6902 |
. . . . . . 7
⊢
(((coeff‘𝐹):ℕ0⟶(𝑆 ∪ {0}) ∧ 𝑘 ∈ ℕ0)
→ ((coeff‘𝐹)‘𝑘) ∈ (𝑆 ∪ {0})) |
21 | 16, 17, 20 | syl2an 599 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((coeff‘𝐹)‘𝑘) ∈ (𝑆 ∪ {0})) |
22 | | plycj.3 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (∗‘𝑥) ∈ 𝑆) |
23 | 22 | ralrimiva 3105 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 (∗‘𝑥) ∈ 𝑆) |
24 | | fveq2 6717 |
. . . . . . . . . . . 12
⊢ (𝑥 = ((coeff‘𝐹)‘𝑘) → (∗‘𝑥) = (∗‘((coeff‘𝐹)‘𝑘))) |
25 | 24 | eleq1d 2822 |
. . . . . . . . . . 11
⊢ (𝑥 = ((coeff‘𝐹)‘𝑘) → ((∗‘𝑥) ∈ 𝑆 ↔ (∗‘((coeff‘𝐹)‘𝑘)) ∈ 𝑆)) |
26 | 25 | rspccv 3534 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝑆 (∗‘𝑥) ∈ 𝑆 → (((coeff‘𝐹)‘𝑘) ∈ 𝑆 → (∗‘((coeff‘𝐹)‘𝑘)) ∈ 𝑆)) |
27 | 23, 26 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (((coeff‘𝐹)‘𝑘) ∈ 𝑆 → (∗‘((coeff‘𝐹)‘𝑘)) ∈ 𝑆)) |
28 | | elsni 4558 |
. . . . . . . . . . . . 13
⊢
(((coeff‘𝐹)‘𝑘) ∈ {0} → ((coeff‘𝐹)‘𝑘) = 0) |
29 | 28 | fveq2d 6721 |
. . . . . . . . . . . 12
⊢
(((coeff‘𝐹)‘𝑘) ∈ {0} →
(∗‘((coeff‘𝐹)‘𝑘)) = (∗‘0)) |
30 | | cj0 14721 |
. . . . . . . . . . . 12
⊢
(∗‘0) = 0 |
31 | 29, 30 | eqtrdi 2794 |
. . . . . . . . . . 11
⊢
(((coeff‘𝐹)‘𝑘) ∈ {0} →
(∗‘((coeff‘𝐹)‘𝑘)) = 0) |
32 | | fvex 6730 |
. . . . . . . . . . . 12
⊢
(∗‘((coeff‘𝐹)‘𝑘)) ∈ V |
33 | 32 | elsn 4556 |
. . . . . . . . . . 11
⊢
((∗‘((coeff‘𝐹)‘𝑘)) ∈ {0} ↔
(∗‘((coeff‘𝐹)‘𝑘)) = 0) |
34 | 31, 33 | sylibr 237 |
. . . . . . . . . 10
⊢
(((coeff‘𝐹)‘𝑘) ∈ {0} →
(∗‘((coeff‘𝐹)‘𝑘)) ∈ {0}) |
35 | 34 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (((coeff‘𝐹)‘𝑘) ∈ {0} →
(∗‘((coeff‘𝐹)‘𝑘)) ∈ {0})) |
36 | 27, 35 | orim12d 965 |
. . . . . . . 8
⊢ (𝜑 → ((((coeff‘𝐹)‘𝑘) ∈ 𝑆 ∨ ((coeff‘𝐹)‘𝑘) ∈ {0}) →
((∗‘((coeff‘𝐹)‘𝑘)) ∈ 𝑆 ∨ (∗‘((coeff‘𝐹)‘𝑘)) ∈ {0}))) |
37 | | elun 4063 |
. . . . . . . 8
⊢
(((coeff‘𝐹)‘𝑘) ∈ (𝑆 ∪ {0}) ↔ (((coeff‘𝐹)‘𝑘) ∈ 𝑆 ∨ ((coeff‘𝐹)‘𝑘) ∈ {0})) |
38 | | elun 4063 |
. . . . . . . 8
⊢
((∗‘((coeff‘𝐹)‘𝑘)) ∈ (𝑆 ∪ {0}) ↔
((∗‘((coeff‘𝐹)‘𝑘)) ∈ 𝑆 ∨ (∗‘((coeff‘𝐹)‘𝑘)) ∈ {0})) |
39 | 36, 37, 38 | 3imtr4g 299 |
. . . . . . 7
⊢ (𝜑 → (((coeff‘𝐹)‘𝑘) ∈ (𝑆 ∪ {0}) →
(∗‘((coeff‘𝐹)‘𝑘)) ∈ (𝑆 ∪ {0}))) |
40 | 39 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → (((coeff‘𝐹)‘𝑘) ∈ (𝑆 ∪ {0}) →
(∗‘((coeff‘𝐹)‘𝑘)) ∈ (𝑆 ∪ {0}))) |
41 | 21, 40 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) →
(∗‘((coeff‘𝐹)‘𝑘)) ∈ (𝑆 ∪ {0})) |
42 | 19, 41 | eqeltrd 2838 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...𝑁)) → ((∗ ∘
(coeff‘𝐹))‘𝑘) ∈ (𝑆 ∪ {0})) |
43 | 11, 14, 42 | elplyd 25096 |
. . 3
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...𝑁)(((∗ ∘ (coeff‘𝐹))‘𝑘) · (𝑧↑𝑘))) ∈ (Poly‘(𝑆 ∪ {0}))) |
44 | 6, 43 | eqeltrd 2838 |
. 2
⊢ (𝜑 → 𝐺 ∈ (Poly‘(𝑆 ∪ {0}))) |
45 | | plyun0 25091 |
. 2
⊢
(Poly‘(𝑆 ∪
{0})) = (Poly‘𝑆) |
46 | 44, 45 | eleqtrdi 2848 |
1
⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆)) |