Step | Hyp | Ref
| Expression |
1 | | ax-resscn 9993 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
2 | | 1re 10039 |
. . . . . . 7
⊢ 1 ∈
ℝ |
3 | | plyid 23965 |
. . . . . . 7
⊢ ((ℝ
⊆ ℂ ∧ 1 ∈ ℝ) → Xp ∈
(Poly‘ℝ)) |
4 | 1, 2, 3 | mp2an 708 |
. . . . . 6
⊢
Xp ∈ (Poly‘ℝ) |
5 | | plymul02 30623 |
. . . . . . 7
⊢
(Xp ∈ (Poly‘ℝ) →
(0𝑝 ∘𝑓 ·
Xp) = 0𝑝) |
6 | 5 | fveq2d 6195 |
. . . . . 6
⊢
(Xp ∈ (Poly‘ℝ) →
(coeff‘(0𝑝 ∘𝑓 ·
Xp)) = (coeff‘0𝑝)) |
7 | 4, 6 | ax-mp 5 |
. . . . 5
⊢
(coeff‘(0𝑝 ∘𝑓 ·
Xp)) = (coeff‘0𝑝) |
8 | | fconstmpt 5163 |
. . . . . 6
⊢
(ℕ0 × {0}) = (𝑛 ∈ ℕ0 ↦
0) |
9 | | coe0 24012 |
. . . . . 6
⊢
(coeff‘0𝑝) = (ℕ0 ×
{0}) |
10 | | eqidd 2623 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ0
∧ 𝑛 = 0) → 0 =
0) |
11 | | elnnne0 11306 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ ↔ (𝑛 ∈ ℕ0
∧ 𝑛 ≠
0)) |
12 | | df-ne 2795 |
. . . . . . . . . . . 12
⊢ (𝑛 ≠ 0 ↔ ¬ 𝑛 = 0) |
13 | 12 | anbi2i 730 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ0
∧ 𝑛 ≠ 0) ↔
(𝑛 ∈
ℕ0 ∧ ¬ 𝑛 = 0)) |
14 | 11, 13 | bitr2i 265 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ0
∧ ¬ 𝑛 = 0) ↔
𝑛 ∈
ℕ) |
15 | | nnm1nn0 11334 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈
ℕ0) |
16 | 14, 15 | sylbi 207 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ0
∧ ¬ 𝑛 = 0) →
(𝑛 − 1) ∈
ℕ0) |
17 | | eqidd 2623 |
. . . . . . . . . 10
⊢ (𝑚 = (𝑛 − 1) → 0 = 0) |
18 | | fconstmpt 5163 |
. . . . . . . . . . 11
⊢
(ℕ0 × {0}) = (𝑚 ∈ ℕ0 ↦
0) |
19 | 9, 18 | eqtri 2644 |
. . . . . . . . . 10
⊢
(coeff‘0𝑝) = (𝑚 ∈ ℕ0 ↦
0) |
20 | | c0ex 10034 |
. . . . . . . . . 10
⊢ 0 ∈
V |
21 | 17, 19, 20 | fvmpt 6282 |
. . . . . . . . 9
⊢ ((𝑛 − 1) ∈
ℕ0 → ((coeff‘0𝑝)‘(𝑛 − 1)) =
0) |
22 | 16, 21 | syl 17 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ0
∧ ¬ 𝑛 = 0) →
((coeff‘0𝑝)‘(𝑛 − 1)) = 0) |
23 | 10, 22 | ifeqda 4121 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ0
→ if(𝑛 = 0, 0,
((coeff‘0𝑝)‘(𝑛 − 1))) = 0) |
24 | 23 | mpteq2ia 4740 |
. . . . . 6
⊢ (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, 0,
((coeff‘0𝑝)‘(𝑛 − 1)))) = (𝑛 ∈ ℕ0 ↦
0) |
25 | 8, 9, 24 | 3eqtr4ri 2655 |
. . . . 5
⊢ (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, 0,
((coeff‘0𝑝)‘(𝑛 − 1)))) =
(coeff‘0𝑝) |
26 | 7, 25 | eqtr4i 2647 |
. . . 4
⊢
(coeff‘(0𝑝 ∘𝑓 ·
Xp)) = (𝑛
∈ ℕ0 ↦ if(𝑛 = 0, 0,
((coeff‘0𝑝)‘(𝑛 − 1)))) |
27 | | oveq1 6657 |
. . . . 5
⊢ (𝐹 = 0𝑝 →
(𝐹
∘𝑓 · Xp) =
(0𝑝 ∘𝑓 ·
Xp)) |
28 | 27 | fveq2d 6195 |
. . . 4
⊢ (𝐹 = 0𝑝 →
(coeff‘(𝐹
∘𝑓 · Xp)) =
(coeff‘(0𝑝 ∘𝑓 ·
Xp))) |
29 | | simpl 473 |
. . . . . . . 8
⊢ ((𝐹 = 0𝑝 ∧
𝑛 ∈
ℕ0) → 𝐹 = 0𝑝) |
30 | 29 | fveq2d 6195 |
. . . . . . 7
⊢ ((𝐹 = 0𝑝 ∧
𝑛 ∈
ℕ0) → (coeff‘𝐹) =
(coeff‘0𝑝)) |
31 | 30 | fveq1d 6193 |
. . . . . 6
⊢ ((𝐹 = 0𝑝 ∧
𝑛 ∈
ℕ0) → ((coeff‘𝐹)‘(𝑛 − 1)) =
((coeff‘0𝑝)‘(𝑛 − 1))) |
32 | 31 | ifeq2d 4105 |
. . . . 5
⊢ ((𝐹 = 0𝑝 ∧
𝑛 ∈
ℕ0) → if(𝑛 = 0, 0, ((coeff‘𝐹)‘(𝑛 − 1))) = if(𝑛 = 0, 0,
((coeff‘0𝑝)‘(𝑛 − 1)))) |
33 | 32 | mpteq2dva 4744 |
. . . 4
⊢ (𝐹 = 0𝑝 →
(𝑛 ∈
ℕ0 ↦ if(𝑛 = 0, 0, ((coeff‘𝐹)‘(𝑛 − 1)))) = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, 0,
((coeff‘0𝑝)‘(𝑛 − 1))))) |
34 | 26, 28, 33 | 3eqtr4a 2682 |
. . 3
⊢ (𝐹 = 0𝑝 →
(coeff‘(𝐹
∘𝑓 · Xp)) = (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, 0,
((coeff‘𝐹)‘(𝑛 − 1))))) |
35 | 34 | adantl 482 |
. 2
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝐹 =
0𝑝) → (coeff‘(𝐹 ∘𝑓 ·
Xp)) = (𝑛
∈ ℕ0 ↦ if(𝑛 = 0, 0, ((coeff‘𝐹)‘(𝑛 − 1))))) |
36 | | simpl 473 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ ¬ 𝐹 =
0𝑝) → 𝐹 ∈
(Poly‘ℝ)) |
37 | | elsng 4191 |
. . . . . 6
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝐹 ∈
{0𝑝} ↔ 𝐹 = 0𝑝)) |
38 | 37 | notbid 308 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (¬ 𝐹 ∈
{0𝑝} ↔ ¬ 𝐹 = 0𝑝)) |
39 | 38 | biimpar 502 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ ¬ 𝐹 =
0𝑝) → ¬ 𝐹 ∈
{0𝑝}) |
40 | 36, 39 | eldifd 3585 |
. . 3
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ ¬ 𝐹 =
0𝑝) → 𝐹 ∈ ((Poly‘ℝ) ∖
{0𝑝})) |
41 | | plymulx0 30624 |
. . 3
⊢ (𝐹 ∈ ((Poly‘ℝ)
∖ {0𝑝}) → (coeff‘(𝐹 ∘𝑓 ·
Xp)) = (𝑛
∈ ℕ0 ↦ if(𝑛 = 0, 0, ((coeff‘𝐹)‘(𝑛 − 1))))) |
42 | 40, 41 | syl 17 |
. 2
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ ¬ 𝐹 =
0𝑝) → (coeff‘(𝐹 ∘𝑓 ·
Xp)) = (𝑛
∈ ℕ0 ↦ if(𝑛 = 0, 0, ((coeff‘𝐹)‘(𝑛 − 1))))) |
43 | 35, 42 | pm2.61dan 832 |
1
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (coeff‘(𝐹
∘𝑓 · Xp)) = (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, 0,
((coeff‘𝐹)‘(𝑛 − 1))))) |