| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | plycj.4 | . . . 4
⊢ (𝜑 → 𝐹 ∈ (Poly‘𝑆)) | 
| 2 |  | eqid 2736 | . . . . 5
⊢
(deg‘𝐹) =
(deg‘𝐹) | 
| 3 |  | plycj.2 | . . . . 5
⊢ 𝐺 = ((∗ ∘ 𝐹) ∘
∗) | 
| 4 |  | eqid 2736 | . . . . 5
⊢
(coeff‘𝐹) =
(coeff‘𝐹) | 
| 5 | 2, 3, 4 | plycjlem 26317 | . . . 4
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(deg‘𝐹))(((∗ ∘
(coeff‘𝐹))‘𝑘) · (𝑧↑𝑘)))) | 
| 6 | 1, 5 | syl 17 | . . 3
⊢ (𝜑 → 𝐺 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(deg‘𝐹))(((∗ ∘
(coeff‘𝐹))‘𝑘) · (𝑧↑𝑘)))) | 
| 7 |  | plybss 26234 | . . . . . 6
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝑆 ⊆ ℂ) | 
| 8 | 1, 7 | syl 17 | . . . . 5
⊢ (𝜑 → 𝑆 ⊆ ℂ) | 
| 9 |  | 0cnd 11255 | . . . . . 6
⊢ (𝜑 → 0 ∈
ℂ) | 
| 10 | 9 | snssd 4808 | . . . . 5
⊢ (𝜑 → {0} ⊆
ℂ) | 
| 11 | 8, 10 | unssd 4191 | . . . 4
⊢ (𝜑 → (𝑆 ∪ {0}) ⊆
ℂ) | 
| 12 |  | dgrcl 26273 | . . . . 5
⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘𝐹) ∈
ℕ0) | 
| 13 | 1, 12 | syl 17 | . . . 4
⊢ (𝜑 → (deg‘𝐹) ∈
ℕ0) | 
| 14 | 4 | coef 26270 | . . . . . . 7
⊢ (𝐹 ∈ (Poly‘𝑆) → (coeff‘𝐹):ℕ0⟶(𝑆 ∪ {0})) | 
| 15 | 1, 14 | syl 17 | . . . . . 6
⊢ (𝜑 → (coeff‘𝐹):ℕ0⟶(𝑆 ∪ {0})) | 
| 16 |  | elfznn0 13661 | . . . . . 6
⊢ (𝑘 ∈ (0...(deg‘𝐹)) → 𝑘 ∈ ℕ0) | 
| 17 |  | fvco3 7007 | . . . . . 6
⊢
(((coeff‘𝐹):ℕ0⟶(𝑆 ∪ {0}) ∧ 𝑘 ∈ ℕ0)
→ ((∗ ∘ (coeff‘𝐹))‘𝑘) = (∗‘((coeff‘𝐹)‘𝑘))) | 
| 18 | 15, 16, 17 | syl2an 596 | . . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(deg‘𝐹))) → ((∗ ∘
(coeff‘𝐹))‘𝑘) = (∗‘((coeff‘𝐹)‘𝑘))) | 
| 19 |  | ffvelcdm 7100 | . . . . . . 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 3145 | . . . . . . . . . 10
⊢ (𝜑 → ∀𝑥 ∈ 𝑆 (∗‘𝑥) ∈ 𝑆) | 
| 23 |  | fveq2 6905 | . . . . . . . . . . . 12
⊢ (𝑥 = ((coeff‘𝐹)‘𝑘) → (∗‘𝑥) = (∗‘((coeff‘𝐹)‘𝑘))) | 
| 24 | 23 | eleq1d 2825 | . . . . . . . . . . 11
⊢ (𝑥 = ((coeff‘𝐹)‘𝑘) → ((∗‘𝑥) ∈ 𝑆 ↔ (∗‘((coeff‘𝐹)‘𝑘)) ∈ 𝑆)) | 
| 25 | 24 | rspccv 3618 | . . . . . . . . . 10
⊢
(∀𝑥 ∈
𝑆 (∗‘𝑥) ∈ 𝑆 → (((coeff‘𝐹)‘𝑘) ∈ 𝑆 → (∗‘((coeff‘𝐹)‘𝑘)) ∈ 𝑆)) | 
| 26 | 22, 25 | syl 17 | . . . . . . . . 9
⊢ (𝜑 → (((coeff‘𝐹)‘𝑘) ∈ 𝑆 → (∗‘((coeff‘𝐹)‘𝑘)) ∈ 𝑆)) | 
| 27 |  | elsni 4642 | . . . . . . . . . . . . 13
⊢
(((coeff‘𝐹)‘𝑘) ∈ {0} → ((coeff‘𝐹)‘𝑘) = 0) | 
| 28 | 27 | fveq2d 6909 | . . . . . . . . . . . 12
⊢
(((coeff‘𝐹)‘𝑘) ∈ {0} →
(∗‘((coeff‘𝐹)‘𝑘)) = (∗‘0)) | 
| 29 |  | cj0 15198 | . . . . . . . . . . . 12
⊢
(∗‘0) = 0 | 
| 30 | 28, 29 | eqtrdi 2792 | . . . . . . . . . . 11
⊢
(((coeff‘𝐹)‘𝑘) ∈ {0} →
(∗‘((coeff‘𝐹)‘𝑘)) = 0) | 
| 31 |  | fvex 6918 | . . . . . . . . . . . 12
⊢
(∗‘((coeff‘𝐹)‘𝑘)) ∈ V | 
| 32 | 31 | elsn 4640 | . . . . . . . . . . 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 4152 | . . . . . . . 8
⊢
(((coeff‘𝐹)‘𝑘) ∈ (𝑆 ∪ {0}) ↔ (((coeff‘𝐹)‘𝑘) ∈ 𝑆 ∨ ((coeff‘𝐹)‘𝑘) ∈ {0})) | 
| 37 |  | elun 4152 | . . . . . . . 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 2840 | . . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (0...(deg‘𝐹))) → ((∗ ∘
(coeff‘𝐹))‘𝑘) ∈ (𝑆 ∪ {0})) | 
| 42 | 11, 13, 41 | elplyd 26242 | . . 3
⊢ (𝜑 → (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(deg‘𝐹))(((∗ ∘
(coeff‘𝐹))‘𝑘) · (𝑧↑𝑘))) ∈ (Poly‘(𝑆 ∪ {0}))) | 
| 43 | 6, 42 | eqeltrd 2840 | . 2
⊢ (𝜑 → 𝐺 ∈ (Poly‘(𝑆 ∪ {0}))) | 
| 44 |  | plyun0 26237 | . 2
⊢
(Poly‘(𝑆 ∪
{0})) = (Poly‘𝑆) | 
| 45 | 43, 44 | eleqtrdi 2850 | 1
⊢ (𝜑 → 𝐺 ∈ (Poly‘𝑆)) |