Step | Hyp | Ref
| Expression |
1 | | eqid 2733 |
. . . . . . . 8
⊢
(coeff‘𝐹) =
(coeff‘𝐹) |
2 | | eqid 2733 |
. . . . . . . 8
⊢
(deg‘𝐹) =
(deg‘𝐹) |
3 | 1, 2 | coeid 25427 |
. . . . . . 7
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(deg‘𝐹))(((coeff‘𝐹)‘𝑘) · (𝑧↑𝑘)))) |
4 | 3 | adantr 480 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (deg‘𝐹) = 0) → 𝐹 = (𝑧 ∈ ℂ ↦ Σ𝑘 ∈ (0...(deg‘𝐹))(((coeff‘𝐹)‘𝑘) · (𝑧↑𝑘)))) |
5 | | simplr 765 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (deg‘𝐹) = 0) ∧ 𝑧 ∈ ℂ) → (deg‘𝐹) = 0) |
6 | 5 | oveq2d 7311 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (deg‘𝐹) = 0) ∧ 𝑧 ∈ ℂ) → (0...(deg‘𝐹)) = (0...0)) |
7 | 6 | sumeq1d 15441 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (deg‘𝐹) = 0) ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...(deg‘𝐹))(((coeff‘𝐹)‘𝑘) · (𝑧↑𝑘)) = Σ𝑘 ∈ (0...0)(((coeff‘𝐹)‘𝑘) · (𝑧↑𝑘))) |
8 | | 0z 12358 |
. . . . . . . . . 10
⊢ 0 ∈
ℤ |
9 | | exp0 13814 |
. . . . . . . . . . . . . 14
⊢ (𝑧 ∈ ℂ → (𝑧↑0) = 1) |
10 | 9 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (deg‘𝐹) = 0) ∧ 𝑧 ∈ ℂ) → (𝑧↑0) = 1) |
11 | 10 | oveq2d 7311 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (deg‘𝐹) = 0) ∧ 𝑧 ∈ ℂ) → (((coeff‘𝐹)‘0) · (𝑧↑0)) = (((coeff‘𝐹)‘0) ·
1)) |
12 | 1 | coef3 25421 |
. . . . . . . . . . . . . . 15
⊢ (𝐹 ∈ (Poly‘𝑆) → (coeff‘𝐹):ℕ0⟶ℂ) |
13 | | 0nn0 12276 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℕ0 |
14 | | ffvelcdm 6979 |
. . . . . . . . . . . . . . 15
⊢
(((coeff‘𝐹):ℕ0⟶ℂ ∧ 0
∈ ℕ0) → ((coeff‘𝐹)‘0) ∈ ℂ) |
15 | 12, 13, 14 | sylancl 585 |
. . . . . . . . . . . . . 14
⊢ (𝐹 ∈ (Poly‘𝑆) → ((coeff‘𝐹)‘0) ∈
ℂ) |
16 | 15 | ad2antrr 722 |
. . . . . . . . . . . . 13
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (deg‘𝐹) = 0) ∧ 𝑧 ∈ ℂ) → ((coeff‘𝐹)‘0) ∈
ℂ) |
17 | 16 | mulid1d 11020 |
. . . . . . . . . . . 12
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (deg‘𝐹) = 0) ∧ 𝑧 ∈ ℂ) → (((coeff‘𝐹)‘0) · 1) =
((coeff‘𝐹)‘0)) |
18 | 11, 17 | eqtrd 2773 |
. . . . . . . . . . 11
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (deg‘𝐹) = 0) ∧ 𝑧 ∈ ℂ) → (((coeff‘𝐹)‘0) · (𝑧↑0)) = ((coeff‘𝐹)‘0)) |
19 | 18, 16 | eqeltrd 2834 |
. . . . . . . . . 10
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (deg‘𝐹) = 0) ∧ 𝑧 ∈ ℂ) → (((coeff‘𝐹)‘0) · (𝑧↑0)) ∈
ℂ) |
20 | | fveq2 6792 |
. . . . . . . . . . . 12
⊢ (𝑘 = 0 → ((coeff‘𝐹)‘𝑘) = ((coeff‘𝐹)‘0)) |
21 | | oveq2 7303 |
. . . . . . . . . . . 12
⊢ (𝑘 = 0 → (𝑧↑𝑘) = (𝑧↑0)) |
22 | 20, 21 | oveq12d 7313 |
. . . . . . . . . . 11
⊢ (𝑘 = 0 → (((coeff‘𝐹)‘𝑘) · (𝑧↑𝑘)) = (((coeff‘𝐹)‘0) · (𝑧↑0))) |
23 | 22 | fsum1 15487 |
. . . . . . . . . 10
⊢ ((0
∈ ℤ ∧ (((coeff‘𝐹)‘0) · (𝑧↑0)) ∈ ℂ) → Σ𝑘 ∈
(0...0)(((coeff‘𝐹)‘𝑘) · (𝑧↑𝑘)) = (((coeff‘𝐹)‘0) · (𝑧↑0))) |
24 | 8, 19, 23 | sylancr 586 |
. . . . . . . . 9
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (deg‘𝐹) = 0) ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈
(0...0)(((coeff‘𝐹)‘𝑘) · (𝑧↑𝑘)) = (((coeff‘𝐹)‘0) · (𝑧↑0))) |
25 | 24, 18 | eqtrd 2773 |
. . . . . . . 8
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (deg‘𝐹) = 0) ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈
(0...0)(((coeff‘𝐹)‘𝑘) · (𝑧↑𝑘)) = ((coeff‘𝐹)‘0)) |
26 | 7, 25 | eqtrd 2773 |
. . . . . . 7
⊢ (((𝐹 ∈ (Poly‘𝑆) ∧ (deg‘𝐹) = 0) ∧ 𝑧 ∈ ℂ) → Σ𝑘 ∈ (0...(deg‘𝐹))(((coeff‘𝐹)‘𝑘) · (𝑧↑𝑘)) = ((coeff‘𝐹)‘0)) |
27 | 26 | mpteq2dva 5177 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (deg‘𝐹) = 0) → (𝑧 ∈ ℂ ↦
Σ𝑘 ∈
(0...(deg‘𝐹))(((coeff‘𝐹)‘𝑘) · (𝑧↑𝑘))) = (𝑧 ∈ ℂ ↦ ((coeff‘𝐹)‘0))) |
28 | 4, 27 | eqtrd 2773 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (deg‘𝐹) = 0) → 𝐹 = (𝑧 ∈ ℂ ↦ ((coeff‘𝐹)‘0))) |
29 | | fconstmpt 5651 |
. . . . 5
⊢ (ℂ
× {((coeff‘𝐹)‘0)}) = (𝑧 ∈ ℂ ↦ ((coeff‘𝐹)‘0)) |
30 | 28, 29 | eqtr4di 2791 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (deg‘𝐹) = 0) → 𝐹 = (ℂ × {((coeff‘𝐹)‘0)})) |
31 | 30 | fveq1d 6794 |
. . . . . . 7
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (deg‘𝐹) = 0) → (𝐹‘0) = ((ℂ ×
{((coeff‘𝐹)‘0)})‘0)) |
32 | | 0cn 10995 |
. . . . . . . 8
⊢ 0 ∈
ℂ |
33 | | fvex 6805 |
. . . . . . . . 9
⊢
((coeff‘𝐹)‘0) ∈ V |
34 | 33 | fvconst2 7099 |
. . . . . . . 8
⊢ (0 ∈
ℂ → ((ℂ × {((coeff‘𝐹)‘0)})‘0) = ((coeff‘𝐹)‘0)) |
35 | 32, 34 | ax-mp 5 |
. . . . . . 7
⊢ ((ℂ
× {((coeff‘𝐹)‘0)})‘0) = ((coeff‘𝐹)‘0) |
36 | 31, 35 | eqtrdi 2789 |
. . . . . 6
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (deg‘𝐹) = 0) → (𝐹‘0) = ((coeff‘𝐹)‘0)) |
37 | 36 | sneqd 4576 |
. . . . 5
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (deg‘𝐹) = 0) → {(𝐹‘0)} =
{((coeff‘𝐹)‘0)}) |
38 | 37 | xpeq2d 5621 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (deg‘𝐹) = 0) → (ℂ ×
{(𝐹‘0)}) = (ℂ
× {((coeff‘𝐹)‘0)})) |
39 | 30, 38 | eqtr4d 2776 |
. . 3
⊢ ((𝐹 ∈ (Poly‘𝑆) ∧ (deg‘𝐹) = 0) → 𝐹 = (ℂ × {(𝐹‘0)})) |
40 | 39 | ex 412 |
. 2
⊢ (𝐹 ∈ (Poly‘𝑆) → ((deg‘𝐹) = 0 → 𝐹 = (ℂ × {(𝐹‘0)}))) |
41 | | plyf 25387 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘𝑆) → 𝐹:ℂ⟶ℂ) |
42 | | ffvelcdm 6979 |
. . . . 5
⊢ ((𝐹:ℂ⟶ℂ ∧ 0
∈ ℂ) → (𝐹‘0) ∈ ℂ) |
43 | 41, 32, 42 | sylancl 585 |
. . . 4
⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹‘0) ∈ ℂ) |
44 | | 0dgr 25434 |
. . . 4
⊢ ((𝐹‘0) ∈ ℂ →
(deg‘(ℂ × {(𝐹‘0)})) = 0) |
45 | 43, 44 | syl 17 |
. . 3
⊢ (𝐹 ∈ (Poly‘𝑆) → (deg‘(ℂ
× {(𝐹‘0)})) =
0) |
46 | | fveqeq2 6801 |
. . 3
⊢ (𝐹 = (ℂ × {(𝐹‘0)}) →
((deg‘𝐹) = 0 ↔
(deg‘(ℂ × {(𝐹‘0)})) = 0)) |
47 | 45, 46 | syl5ibrcom 246 |
. 2
⊢ (𝐹 ∈ (Poly‘𝑆) → (𝐹 = (ℂ × {(𝐹‘0)}) → (deg‘𝐹) = 0)) |
48 | 40, 47 | impbid 211 |
1
⊢ (𝐹 ∈ (Poly‘𝑆) → ((deg‘𝐹) = 0 ↔ 𝐹 = (ℂ × {(𝐹‘0)}))) |