Step | Hyp | Ref
| Expression |
1 | | ax-resscn 10617 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
2 | | 1re 10664 |
. . . . . . 7
⊢ 1 ∈
ℝ |
3 | | plyid 24890 |
. . . . . . 7
⊢ ((ℝ
⊆ ℂ ∧ 1 ∈ ℝ) → Xp ∈
(Poly‘ℝ)) |
4 | 1, 2, 3 | mp2an 692 |
. . . . . 6
⊢
Xp ∈ (Poly‘ℝ) |
5 | | plymul02 32029 |
. . . . . . 7
⊢
(Xp ∈ (Poly‘ℝ) →
(0𝑝 ∘f · Xp) =
0𝑝) |
6 | 5 | fveq2d 6655 |
. . . . . 6
⊢
(Xp ∈ (Poly‘ℝ) →
(coeff‘(0𝑝 ∘f ·
Xp)) = (coeff‘0𝑝)) |
7 | 4, 6 | ax-mp 5 |
. . . . 5
⊢
(coeff‘(0𝑝 ∘f ·
Xp)) = (coeff‘0𝑝) |
8 | | fconstmpt 5576 |
. . . . . 6
⊢
(ℕ0 × {0}) = (𝑛 ∈ ℕ0 ↦
0) |
9 | | coe0 24937 |
. . . . . 6
⊢
(coeff‘0𝑝) = (ℕ0 ×
{0}) |
10 | | eqidd 2760 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ0
∧ 𝑛 = 0) → 0 =
0) |
11 | | elnnne0 11933 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ ↔ (𝑛 ∈ ℕ0
∧ 𝑛 ≠
0)) |
12 | | df-ne 2950 |
. . . . . . . . . . . 12
⊢ (𝑛 ≠ 0 ↔ ¬ 𝑛 = 0) |
13 | 12 | anbi2i 626 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ0
∧ 𝑛 ≠ 0) ↔
(𝑛 ∈
ℕ0 ∧ ¬ 𝑛 = 0)) |
14 | 11, 13 | bitr2i 279 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ0
∧ ¬ 𝑛 = 0) ↔
𝑛 ∈
ℕ) |
15 | | nnm1nn0 11960 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈
ℕ0) |
16 | 14, 15 | sylbi 220 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ0
∧ ¬ 𝑛 = 0) →
(𝑛 − 1) ∈
ℕ0) |
17 | | eqidd 2760 |
. . . . . . . . . 10
⊢ (𝑚 = (𝑛 − 1) → 0 = 0) |
18 | | fconstmpt 5576 |
. . . . . . . . . . 11
⊢
(ℕ0 × {0}) = (𝑚 ∈ ℕ0 ↦
0) |
19 | 9, 18 | eqtri 2782 |
. . . . . . . . . 10
⊢
(coeff‘0𝑝) = (𝑚 ∈ ℕ0 ↦
0) |
20 | | c0ex 10658 |
. . . . . . . . . 10
⊢ 0 ∈
V |
21 | 17, 19, 20 | fvmpt 6752 |
. . . . . . . . 9
⊢ ((𝑛 − 1) ∈
ℕ0 → ((coeff‘0𝑝)‘(𝑛 − 1)) =
0) |
22 | 16, 21 | syl 17 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ0
∧ ¬ 𝑛 = 0) →
((coeff‘0𝑝)‘(𝑛 − 1)) = 0) |
23 | 10, 22 | ifeqda 4449 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ0
→ if(𝑛 = 0, 0,
((coeff‘0𝑝)‘(𝑛 − 1))) = 0) |
24 | 23 | mpteq2ia 5116 |
. . . . . 6
⊢ (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, 0,
((coeff‘0𝑝)‘(𝑛 − 1)))) = (𝑛 ∈ ℕ0 ↦
0) |
25 | 8, 9, 24 | 3eqtr4ri 2793 |
. . . . 5
⊢ (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, 0,
((coeff‘0𝑝)‘(𝑛 − 1)))) =
(coeff‘0𝑝) |
26 | 7, 25 | eqtr4i 2785 |
. . . 4
⊢
(coeff‘(0𝑝 ∘f ·
Xp)) = (𝑛
∈ ℕ0 ↦ if(𝑛 = 0, 0,
((coeff‘0𝑝)‘(𝑛 − 1)))) |
27 | | fvoveq1 7166 |
. . . 4
⊢ (𝐹 = 0𝑝 →
(coeff‘(𝐹
∘f · Xp)) =
(coeff‘(0𝑝 ∘f ·
Xp))) |
28 | | simpl 487 |
. . . . . . . 8
⊢ ((𝐹 = 0𝑝 ∧
𝑛 ∈
ℕ0) → 𝐹 = 0𝑝) |
29 | 28 | fveq2d 6655 |
. . . . . . 7
⊢ ((𝐹 = 0𝑝 ∧
𝑛 ∈
ℕ0) → (coeff‘𝐹) =
(coeff‘0𝑝)) |
30 | 29 | fveq1d 6653 |
. . . . . 6
⊢ ((𝐹 = 0𝑝 ∧
𝑛 ∈
ℕ0) → ((coeff‘𝐹)‘(𝑛 − 1)) =
((coeff‘0𝑝)‘(𝑛 − 1))) |
31 | 30 | ifeq2d 4433 |
. . . . 5
⊢ ((𝐹 = 0𝑝 ∧
𝑛 ∈
ℕ0) → if(𝑛 = 0, 0, ((coeff‘𝐹)‘(𝑛 − 1))) = if(𝑛 = 0, 0,
((coeff‘0𝑝)‘(𝑛 − 1)))) |
32 | 31 | mpteq2dva 5120 |
. . . 4
⊢ (𝐹 = 0𝑝 →
(𝑛 ∈
ℕ0 ↦ if(𝑛 = 0, 0, ((coeff‘𝐹)‘(𝑛 − 1)))) = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, 0,
((coeff‘0𝑝)‘(𝑛 − 1))))) |
33 | 26, 27, 32 | 3eqtr4a 2820 |
. . 3
⊢ (𝐹 = 0𝑝 →
(coeff‘(𝐹
∘f · Xp)) = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, 0, ((coeff‘𝐹)‘(𝑛 − 1))))) |
34 | 33 | adantl 486 |
. 2
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝐹 =
0𝑝) → (coeff‘(𝐹 ∘f ·
Xp)) = (𝑛
∈ ℕ0 ↦ if(𝑛 = 0, 0, ((coeff‘𝐹)‘(𝑛 − 1))))) |
35 | | simpl 487 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ ¬ 𝐹 =
0𝑝) → 𝐹 ∈
(Poly‘ℝ)) |
36 | | elsng 4529 |
. . . . . 6
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝐹 ∈
{0𝑝} ↔ 𝐹 = 0𝑝)) |
37 | 36 | notbid 322 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (¬ 𝐹 ∈
{0𝑝} ↔ ¬ 𝐹 = 0𝑝)) |
38 | 37 | biimpar 482 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ ¬ 𝐹 =
0𝑝) → ¬ 𝐹 ∈
{0𝑝}) |
39 | 35, 38 | eldifd 3865 |
. . 3
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ ¬ 𝐹 =
0𝑝) → 𝐹 ∈ ((Poly‘ℝ) ∖
{0𝑝})) |
40 | | plymulx0 32030 |
. . 3
⊢ (𝐹 ∈ ((Poly‘ℝ)
∖ {0𝑝}) → (coeff‘(𝐹 ∘f ·
Xp)) = (𝑛
∈ ℕ0 ↦ if(𝑛 = 0, 0, ((coeff‘𝐹)‘(𝑛 − 1))))) |
41 | 39, 40 | syl 17 |
. 2
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ ¬ 𝐹 =
0𝑝) → (coeff‘(𝐹 ∘f ·
Xp)) = (𝑛
∈ ℕ0 ↦ if(𝑛 = 0, 0, ((coeff‘𝐹)‘(𝑛 − 1))))) |
42 | 34, 41 | pm2.61dan 813 |
1
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (coeff‘(𝐹
∘f · Xp)) = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, 0, ((coeff‘𝐹)‘(𝑛 − 1))))) |