Step | Hyp | Ref
| Expression |
1 | | plycj.4 |
. . . 4
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) |
2 | | eqid 2735 |
. . . . 5
⊢
(deg‘𝐹) =
(deg‘𝐹) |
3 | | plycj.2 |
. . . . 5
⊢ 𝐺 = ((∗ ∘ 𝐹) ∘
∗) |
4 | | eqid 2735 |
. . . . 5
⊢
(coeff‘𝐹) =
(coeff‘𝐹) |
5 | 2, 3, 4 | plycjlem 26331 |
. . . 4
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(deg‘𝐹))(((∗ ∘
(coeff‘𝐹))‘𝑘) · (𝑧↑𝑘)))) |
6 | 1, 5 | syl 17 |
. . 3
⊢ (𝜑 → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(deg‘𝐹))(((∗ ∘
(coeff‘𝐹))‘𝑘) · (𝑧↑𝑘)))) |
7 | | plybss 26248 |
. . . . . 6
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝑆 ⊆ ℂ) |
8 | 1, 7 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝑆 ⊆ ℂ) |
9 | | 0cnd 11252 |
. . . . . 6
⊢ (𝜑 → 0 ∈
ℂ) |
10 | 9 | snssd 4814 |
. . . . 5
⊢ (𝜑 → {0} ⊆
ℂ) |
11 | 8, 10 | unssd 4202 |
. . . 4
⊢ (𝜑 → (𝑆 ∪ {0}) ⊆
ℂ) |
12 | | dgrcl 26287 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) ∈
ℕ0) |
13 | 1, 12 | syl 17 |
. . . 4
⊢ (𝜑 → (deg‘𝐹) ∈
ℕ0) |
14 | 4 | coef 26284 |
. . . . . . 7
⊢ (𝐹 ∈ (Poly‘𝑆) → (coeff‘𝐹):ℕ0⟶(𝑆 ∪ {0})) |
15 | 1, 14 | syl 17 |
. . . . . 6
⊢ (𝜑 → (coeff‘𝐹):ℕ0⟶(𝑆 ∪ {0})) |
16 | | elfznn0 13657 |
. . . . . 6
⊢ (𝑘 ∈ (0...(deg‘𝐹)) → 𝑘 ∈ ℕ0) |
17 | | fvco3 7008 |
. . . . . 6
⊢
(((coeff‘𝐹):ℕ0⟶(𝑆 ∪ {0}) ∧ 𝑘 ∈ ℕ0)
→ ((∗ ∘ (coeff‘𝐹))‘𝑘) = (∗‘((coeff‘𝐹)‘𝑘))) |
18 | 15, 16, 17 | syl2an 596 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(deg‘𝐹))) → ((∗ ∘
(coeff‘𝐹))‘𝑘) = (∗‘((coeff‘𝐹)‘𝑘))) |
19 | | ffvelcdm 7101 |
. . . . . . 7
⊢
(((coeff‘𝐹):ℕ0⟶(𝑆 ∪ {0}) ∧ 𝑘 ∈ ℕ0)
→ ((coeff‘𝐹)‘𝑘) ∈ (𝑆 ∪ {0})) |
20 | 15, 16, 19 | syl2an 596 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(deg‘𝐹))) → ((coeff‘𝐹)‘𝑘) ∈ (𝑆 ∪ {0})) |
21 | | plycj.3 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑆) → (∗‘𝑥) ∈ 𝑆) |
22 | 21 | ralrimiva 3144 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 (∗‘𝑥) ∈ 𝑆) |
23 | | fveq2 6907 |
. . . . . . . . . . . 12
⊢ (𝑥 = ((coeff‘𝐹)‘𝑘) → (∗‘𝑥) = (∗‘((coeff‘𝐹)‘𝑘))) |
24 | 23 | eleq1d 2824 |
. . . . . . . . . . 11
⊢ (𝑥 = ((coeff‘𝐹)‘𝑘) → ((∗‘𝑥) ∈ 𝑆 ↔ (∗‘((coeff‘𝐹)‘𝑘)) ∈ 𝑆)) |
25 | 24 | rspccv 3619 |
. . . . . . . . . 10
⊢
(∀𝑥 ∈
𝑆 (∗‘𝑥) ∈ 𝑆 → (((coeff‘𝐹)‘𝑘) ∈ 𝑆 → (∗‘((coeff‘𝐹)‘𝑘)) ∈ 𝑆)) |
26 | 22, 25 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (((coeff‘𝐹)‘𝑘) ∈ 𝑆 → (∗‘((coeff‘𝐹)‘𝑘)) ∈ 𝑆)) |
27 | | elsni 4648 |
. . . . . . . . . . . . 13
⊢
(((coeff‘𝐹)‘𝑘) ∈ {0} → ((coeff‘𝐹)‘𝑘) = 0) |
28 | 27 | fveq2d 6911 |
. . . . . . . . . . . 12
⊢
(((coeff‘𝐹)‘𝑘) ∈ {0} →
(∗‘((coeff‘𝐹)‘𝑘)) = (∗‘0)) |
29 | | cj0 15194 |
. . . . . . . . . . . 12
⊢
(∗‘0) = 0 |
30 | 28, 29 | eqtrdi 2791 |
. . . . . . . . . . 11
⊢
(((coeff‘𝐹)‘𝑘) ∈ {0} →
(∗‘((coeff‘𝐹)‘𝑘)) = 0) |
31 | | fvex 6920 |
. . . . . . . . . . . 12
⊢
(∗‘((coeff‘𝐹)‘𝑘)) ∈ V |
32 | 31 | elsn 4646 |
. . . . . . . . . . 11
⊢
((∗‘((coeff‘𝐹)‘𝑘)) ∈ {0} ↔
(∗‘((coeff‘𝐹)‘𝑘)) = 0) |
33 | 30, 32 | sylibr 234 |
. . . . . . . . . 10
⊢
(((coeff‘𝐹)‘𝑘) ∈ {0} →
(∗‘((coeff‘𝐹)‘𝑘)) ∈ {0}) |
34 | 33 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (((coeff‘𝐹)‘𝑘) ∈ {0} →
(∗‘((coeff‘𝐹)‘𝑘)) ∈ {0})) |
35 | 26, 34 | orim12d 966 |
. . . . . . . 8
⊢ (𝜑 → ((((coeff‘𝐹)‘𝑘) ∈ 𝑆 ∨ ((coeff‘𝐹)‘𝑘) ∈ {0}) →
((∗‘((coeff‘𝐹)‘𝑘)) ∈ 𝑆 ∨ (∗‘((coeff‘𝐹)‘𝑘)) ∈ {0}))) |
36 | | elun 4163 |
. . . . . . . 8
⊢
(((coeff‘𝐹)‘𝑘) ∈ (𝑆 ∪ {0}) ↔ (((coeff‘𝐹)‘𝑘) ∈ 𝑆 ∨ ((coeff‘𝐹)‘𝑘) ∈ {0})) |
37 | | elun 4163 |
. . . . . . . 8
⊢
((∗‘((coeff‘𝐹)‘𝑘)) ∈ (𝑆 ∪ {0}) ↔
((∗‘((coeff‘𝐹)‘𝑘)) ∈ 𝑆 ∨ (∗‘((coeff‘𝐹)‘𝑘)) ∈ {0})) |
38 | 35, 36, 37 | 3imtr4g 296 |
. . . . . . 7
⊢ (𝜑 → (((coeff‘𝐹)‘𝑘) ∈ (𝑆 ∪ {0}) →
(∗‘((coeff‘𝐹)‘𝑘)) ∈ (𝑆 ∪ {0}))) |
39 | 38 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(deg‘𝐹))) → (((coeff‘𝐹)‘𝑘) ∈ (𝑆 ∪ {0}) →
(∗‘((coeff‘𝐹)‘𝑘)) ∈ (𝑆 ∪ {0}))) |
40 | 20, 39 | mpd 15 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(deg‘𝐹))) →
(∗‘((coeff‘𝐹)‘𝑘)) ∈ (𝑆 ∪ {0})) |
41 | 18, 40 | eqeltrd 2839 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(deg‘𝐹))) → ((∗ ∘
(coeff‘𝐹))‘𝑘) ∈ (𝑆 ∪ {0})) |
42 | 11, 13, 41 | elplyd 26256 |
. . 3
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(deg‘𝐹))(((∗ ∘
(coeff‘𝐹))‘𝑘) · (𝑧↑𝑘))) ∈ (Poly‘(𝑆 ∪ {0}))) |
43 | 6, 42 | eqeltrd 2839 |
. 2
⊢ (𝜑 → 𝐺 ∈ (Poly‘(𝑆 ∪ {0}))) |
44 | | plyun0 26251 |
. 2
⊢
(Poly‘(𝑆 ∪
{0})) = (Poly‘𝑆) |
45 | 43, 44 | eleqtrdi 2849 |
1
⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆)) |