| Step | Hyp | Ref
| Expression |
| 1 | | ax-resscn 11212 |
. . . . . . 7
⊢ ℝ
⊆ ℂ |
| 2 | | 1re 11261 |
. . . . . . 7
⊢ 1 ∈
ℝ |
| 3 | | plyid 26248 |
. . . . . . 7
⊢ ((ℝ
⊆ ℂ ∧ 1 ∈ ℝ) → Xp ∈
(Poly‘ℝ)) |
| 4 | 1, 2, 3 | mp2an 692 |
. . . . . 6
⊢
Xp ∈ (Poly‘ℝ) |
| 5 | | plymul02 34561 |
. . . . . . 7
⊢
(Xp ∈ (Poly‘ℝ) →
(0𝑝 ∘f · Xp) =
0𝑝) |
| 6 | 5 | fveq2d 6910 |
. . . . . 6
⊢
(Xp ∈ (Poly‘ℝ) →
(coeff‘(0𝑝 ∘f ·
Xp)) = (coeff‘0𝑝)) |
| 7 | 4, 6 | ax-mp 5 |
. . . . 5
⊢
(coeff‘(0𝑝 ∘f ·
Xp)) = (coeff‘0𝑝) |
| 8 | | fconstmpt 5747 |
. . . . . 6
⊢
(ℕ0 × {0}) = (𝑛 ∈ ℕ0 ↦
0) |
| 9 | | coe0 26295 |
. . . . . 6
⊢
(coeff‘0𝑝) = (ℕ0 ×
{0}) |
| 10 | | eqidd 2738 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ0
∧ 𝑛 = 0) → 0 =
0) |
| 11 | | elnnne0 12540 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℕ ↔ (𝑛 ∈ ℕ0
∧ 𝑛 ≠
0)) |
| 12 | | df-ne 2941 |
. . . . . . . . . . . 12
⊢ (𝑛 ≠ 0 ↔ ¬ 𝑛 = 0) |
| 13 | 12 | anbi2i 623 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℕ0
∧ 𝑛 ≠ 0) ↔
(𝑛 ∈
ℕ0 ∧ ¬ 𝑛 = 0)) |
| 14 | 11, 13 | bitr2i 276 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℕ0
∧ ¬ 𝑛 = 0) ↔
𝑛 ∈
ℕ) |
| 15 | | nnm1nn0 12567 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ → (𝑛 − 1) ∈
ℕ0) |
| 16 | 14, 15 | sylbi 217 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℕ0
∧ ¬ 𝑛 = 0) →
(𝑛 − 1) ∈
ℕ0) |
| 17 | | eqidd 2738 |
. . . . . . . . . 10
⊢ (𝑚 = (𝑛 − 1) → 0 = 0) |
| 18 | | fconstmpt 5747 |
. . . . . . . . . . 11
⊢
(ℕ0 × {0}) = (𝑚 ∈ ℕ0 ↦
0) |
| 19 | 9, 18 | eqtri 2765 |
. . . . . . . . . 10
⊢
(coeff‘0𝑝) = (𝑚 ∈ ℕ0 ↦
0) |
| 20 | | c0ex 11255 |
. . . . . . . . . 10
⊢ 0 ∈
V |
| 21 | 17, 19, 20 | fvmpt 7016 |
. . . . . . . . 9
⊢ ((𝑛 − 1) ∈
ℕ0 → ((coeff‘0𝑝)‘(𝑛 − 1)) =
0) |
| 22 | 16, 21 | syl 17 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℕ0
∧ ¬ 𝑛 = 0) →
((coeff‘0𝑝)‘(𝑛 − 1)) = 0) |
| 23 | 10, 22 | ifeqda 4562 |
. . . . . . 7
⊢ (𝑛 ∈ ℕ0
→ if(𝑛 = 0, 0,
((coeff‘0𝑝)‘(𝑛 − 1))) = 0) |
| 24 | 23 | mpteq2ia 5245 |
. . . . . 6
⊢ (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, 0,
((coeff‘0𝑝)‘(𝑛 − 1)))) = (𝑛 ∈ ℕ0 ↦
0) |
| 25 | 8, 9, 24 | 3eqtr4ri 2776 |
. . . . 5
⊢ (𝑛 ∈ ℕ0
↦ if(𝑛 = 0, 0,
((coeff‘0𝑝)‘(𝑛 − 1)))) =
(coeff‘0𝑝) |
| 26 | 7, 25 | eqtr4i 2768 |
. . . 4
⊢
(coeff‘(0𝑝 ∘f ·
Xp)) = (𝑛
∈ ℕ0 ↦ if(𝑛 = 0, 0,
((coeff‘0𝑝)‘(𝑛 − 1)))) |
| 27 | | fvoveq1 7454 |
. . . 4
⊢ (𝐹 = 0𝑝 →
(coeff‘(𝐹
∘f · Xp)) =
(coeff‘(0𝑝 ∘f ·
Xp))) |
| 28 | | simpl 482 |
. . . . . . . 8
⊢ ((𝐹 = 0𝑝 ∧
𝑛 ∈
ℕ0) → 𝐹 = 0𝑝) |
| 29 | 28 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝐹 = 0𝑝 ∧
𝑛 ∈
ℕ0) → (coeff‘𝐹) =
(coeff‘0𝑝)) |
| 30 | 29 | fveq1d 6908 |
. . . . . 6
⊢ ((𝐹 = 0𝑝 ∧
𝑛 ∈
ℕ0) → ((coeff‘𝐹)‘(𝑛 − 1)) =
((coeff‘0𝑝)‘(𝑛 − 1))) |
| 31 | 30 | ifeq2d 4546 |
. . . . 5
⊢ ((𝐹 = 0𝑝 ∧
𝑛 ∈
ℕ0) → if(𝑛 = 0, 0, ((coeff‘𝐹)‘(𝑛 − 1))) = if(𝑛 = 0, 0,
((coeff‘0𝑝)‘(𝑛 − 1)))) |
| 32 | 31 | mpteq2dva 5242 |
. . . 4
⊢ (𝐹 = 0𝑝 →
(𝑛 ∈
ℕ0 ↦ if(𝑛 = 0, 0, ((coeff‘𝐹)‘(𝑛 − 1)))) = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, 0,
((coeff‘0𝑝)‘(𝑛 − 1))))) |
| 33 | 26, 27, 32 | 3eqtr4a 2803 |
. . 3
⊢ (𝐹 = 0𝑝 →
(coeff‘(𝐹
∘f · Xp)) = (𝑛 ∈ ℕ0 ↦ if(𝑛 = 0, 0, ((coeff‘𝐹)‘(𝑛 − 1))))) |
| 34 | 33 | adantl 481 |
. 2
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ 𝐹 =
0𝑝) → (coeff‘(𝐹 ∘f ·
Xp)) = (𝑛
∈ ℕ0 ↦ if(𝑛 = 0, 0, ((coeff‘𝐹)‘(𝑛 − 1))))) |
| 35 | | simpl 482 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ ¬ 𝐹 =
0𝑝) → 𝐹 ∈
(Poly‘ℝ)) |
| 36 | | elsng 4640 |
. . . . . 6
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (𝐹 ∈
{0𝑝} ↔ 𝐹 = 0𝑝)) |
| 37 | 36 | notbid 318 |
. . . . 5
⊢ (𝐹 ∈ (Poly‘ℝ)
→ (¬ 𝐹 ∈
{0𝑝} ↔ ¬ 𝐹 = 0𝑝)) |
| 38 | 37 | biimpar 477 |
. . . 4
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ ¬ 𝐹 =
0𝑝) → ¬ 𝐹 ∈
{0𝑝}) |
| 39 | 35, 38 | eldifd 3962 |
. . 3
⊢ ((𝐹 ∈ (Poly‘ℝ)
∧ ¬ 𝐹 =
0𝑝) → 𝐹 ∈ ((Poly‘ℝ) ∖
{0𝑝})) |
| 40 | | plymulx0 34562 |
. . 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))))) |