Theorem plymulx

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

	Ref	Expression
Assertion	plymulx	⊢ ( 𝐹 ∈ ( Poly ‘ ℝ ) → ( coeff ‘ ( 𝐹 ∘f · Xp ) ) = ( 𝑛 ∈ ℕ0 ↦ if ( 𝑛 = 0 , 0 , ( ( coeff ‘ 𝐹 ) ‘ ( 𝑛 − 1 ) ) ) ) )

Proof

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