Metamath Proof Explorer

Theorem plymulx

Description: Coefficients of a polynomial multiplied by Xp . (Contributed by Thierry Arnoux, 25-Sep-2018)

Ref Expression
Assertion plymulx ⊢ F ∈ Poly ⁡ ℝ → coeff ⁡ F × f X p = n ∈ ℕ 0 ⟼ if n = 0 0 coeff ⁡ F ⁡ n − 1

Proof

Step Hyp Ref Expression
1 ax-resscn ⊢ ℝ ⊆ ℂ
2 1re ⊢ 1 ∈ ℝ
3 plyid ⊢ ℝ ⊆ ℂ ∧ 1 ∈ ℝ → X p ∈ Poly ⁡ ℝ
4 1 2 3 mp2an ⊢ X p ∈ Poly ⁡ ℝ
5 plymul02 ⊢ X p ∈ Poly ⁡ ℝ → 0 𝑝 × f X p = 0 𝑝
6 5 fveq2d ⊢ X p ∈ Poly ⁡ ℝ → coeff ⁡ 0 𝑝 × f X p = coeff ⁡ 0 𝑝
7 4 6 ax-mp ⊢ coeff ⁡ 0 𝑝 × f X p = coeff ⁡ 0 𝑝
8 fconstmpt ⊢ ℕ 0 × 0 = n ∈ ℕ 0 ⟼ 0
9 coe0 ⊢ coeff ⁡ 0 𝑝 = ℕ 0 × 0
10 eqidd ⊢ n ∈ ℕ 0 ∧ n = 0 → 0 = 0
11 elnnne0 ⊢ n ∈ ℕ ↔ n ∈ ℕ 0 ∧ n ≠ 0
12 df-ne ⊢ n ≠ 0 ↔ ¬ n = 0
13 12 anbi2i ⊢ n ∈ ℕ 0 ∧ n ≠ 0 ↔ n ∈ ℕ 0 ∧ ¬ n = 0
14 11 13 bitr2i ⊢ n ∈ ℕ 0 ∧ ¬ n = 0 ↔ n ∈ ℕ
15 nnm1nn0 ⊢ n ∈ ℕ → n − 1 ∈ ℕ 0
16 14 15 sylbi ⊢ n ∈ ℕ 0 ∧ ¬ n = 0 → n − 1 ∈ ℕ 0
17 eqidd ⊢ m = n − 1 → 0 = 0
18 fconstmpt ⊢ ℕ 0 × 0 = m ∈ ℕ 0 ⟼ 0
19 9 18 eqtri ⊢ coeff ⁡ 0 𝑝 = m ∈ ℕ 0 ⟼ 0
20 c0ex ⊢ 0 ∈ V
21 17 19 20 fvmpt ⊢ n − 1 ∈ ℕ 0 → coeff ⁡ 0 𝑝 ⁡ n − 1 = 0
22 16 21 syl ⊢ n ∈ ℕ 0 ∧ ¬ n = 0 → coeff ⁡ 0 𝑝 ⁡ n − 1 = 0
23 10 22 ifeqda ⊢ n ∈ ℕ 0 → if n = 0 0 coeff ⁡ 0 𝑝 ⁡ n − 1 = 0
24 23 mpteq2ia ⊢ n ∈ ℕ 0 ⟼ if n = 0 0 coeff ⁡ 0 𝑝 ⁡ n − 1 = n ∈ ℕ 0 ⟼ 0
25 8 9 24 3eqtr4ri ⊢ n ∈ ℕ 0 ⟼ if n = 0 0 coeff ⁡ 0 𝑝 ⁡ n − 1 = coeff ⁡ 0 𝑝
26 7 25 eqtr4i ⊢ coeff ⁡ 0 𝑝 × f X p = n ∈ ℕ 0 ⟼ if n = 0 0 coeff ⁡ 0 𝑝 ⁡ n − 1
27 fvoveq1 ⊢ F = 0 𝑝 → coeff ⁡ F × f X p = coeff ⁡ 0 𝑝 × f X p
28 simpl ⊢ F = 0 𝑝 ∧ n ∈ ℕ 0 → F = 0 𝑝
29 28 fveq2d ⊢ F = 0 𝑝 ∧ n ∈ ℕ 0 → coeff ⁡ F = coeff ⁡ 0 𝑝
30 29 fveq1d ⊢ F = 0 𝑝 ∧ n ∈ ℕ 0 → coeff ⁡ F ⁡ n − 1 = coeff ⁡ 0 𝑝 ⁡ n − 1
31 30 ifeq2d ⊢ F = 0 𝑝 ∧ n ∈ ℕ 0 → if n = 0 0 coeff ⁡ F ⁡ n − 1 = if n = 0 0 coeff ⁡ 0 𝑝 ⁡ n − 1
32 31 mpteq2dva ⊢ F = 0 𝑝 → n ∈ ℕ 0 ⟼ if n = 0 0 coeff ⁡ F ⁡ n − 1 = n ∈ ℕ 0 ⟼ if n = 0 0 coeff ⁡ 0 𝑝 ⁡ n − 1
33 26 27 32 3eqtr4a ⊢ F = 0 𝑝 → coeff ⁡ F × f X p = n ∈ ℕ 0 ⟼ if n = 0 0 coeff ⁡ F ⁡ n − 1
34 33 adantl ⊢ F ∈ Poly ⁡ ℝ ∧ F = 0 𝑝 → coeff ⁡ F × f X p = n ∈ ℕ 0 ⟼ if n = 0 0 coeff ⁡ F ⁡ n − 1
35 simpl ⊢ F ∈ Poly ⁡ ℝ ∧ ¬ F = 0 𝑝 → F ∈ Poly ⁡ ℝ
36 elsng ⊢ F ∈ Poly ⁡ ℝ → F ∈ 0 𝑝 ↔ F = 0 𝑝
37 36 notbid ⊢ F ∈ Poly ⁡ ℝ → ¬ F ∈ 0 𝑝 ↔ ¬ F = 0 𝑝
38 37 biimpar ⊢ F ∈ Poly ⁡ ℝ ∧ ¬ F = 0 𝑝 → ¬ F ∈ 0 𝑝
39 35 38 eldifd ⊢ F ∈ Poly ⁡ ℝ ∧ ¬ F = 0 𝑝 → F ∈ Poly ⁡ ℝ ∖ 0 𝑝
40 plymulx0 ⊢ F ∈ Poly ⁡ ℝ ∖ 0 𝑝 → coeff ⁡ F × f X p = n ∈ ℕ 0 ⟼ if n = 0 0 coeff ⁡ F ⁡ n − 1
41 39 40 syl ⊢ F ∈ Poly ⁡ ℝ ∧ ¬ F = 0 𝑝 → coeff ⁡ F × f X p = n ∈ ℕ 0 ⟼ if n = 0 0 coeff ⁡ F ⁡ n − 1
42 34 41 pm2.61dan ⊢ F ∈ Poly ⁡ ℝ → coeff ⁡ F × f X p = n ∈ ℕ 0 ⟼ if n = 0 0 coeff ⁡ F ⁡ n − 1