Theorem plymulidp

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

	Ref	Expression
Assertion	plymulidp	$$⊢F\in \mathrm{Poly}\left(ℝ\right)\to \mathrm{coeff}\left(F{\times }_f{X}^p\right)=\left(n\in {\mathbb{N}}_0⟼if\left(n=0,0,\mathrm{coeff}\left(F\right)\left(n-1\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax-resscn	$$⊢ℝ\subseteq ℂ$$
2		1re	$$⊢1\in ℝ$$
3		plyid	$$⊢\left(ℝ\subseteq ℂ\wedge 1\in ℝ\right)\to X^p\in \mathrm{Poly}\left(ℝ\right)$$
4	1 2 3	mp2an	$$⊢X^p\in \mathrm{Poly}\left(ℝ\right)$$
5		plymul02	$$⊢X^p\in \mathrm{Poly}\left(ℝ\right)\to 0_{𝑝}{\times }_f{X}^p=0_{𝑝}$$
6	5	fveq2d	$$⊢X^p\in \mathrm{Poly}\left(ℝ\right)\to \mathrm{coeff}\left(0_{𝑝}{\times }_f{X}^p\right)=\mathrm{coeff}\left(0_{𝑝}\right)$$
7	4 6	ax-mp	$$⊢\mathrm{coeff}\left(0_{𝑝}{\times }_f{X}^p\right)=\mathrm{coeff}\left(0_{𝑝}\right)$$
8		fconstmpt	$$⊢{\mathbb{N}}_0\times \left\{0\right\}=\left(n\in {\mathbb{N}}_0⟼0\right)$$
9		coe0	$$⊢\mathrm{coeff}\left(0_{𝑝}\right)={\mathbb{N}}_0\times \left\{0\right\}$$
10		eqidd	$$⊢\left(n\in {\mathbb{N}}_0\wedge n=0\right)\to 0=0$$
11		elnnne0	$$⊢n\in \mathbb{N}\leftrightarrow \left(n\in {\mathbb{N}}_0\wedge n\ne 0\right)$$
12		df-ne	$$⊢n\ne 0\leftrightarrow \neg n=0$$
13	12	anbi2i	$$⊢\left(n\in {\mathbb{N}}_0\wedge n\ne 0\right)\leftrightarrow \left(n\in {\mathbb{N}}_0\wedge \neg n=0\right)$$
14	11 13	bitr2i	$$⊢\left(n\in {\mathbb{N}}_0\wedge \neg n=0\right)\leftrightarrow n\in \mathbb{N}$$
15		nnm1nn0	$$⊢n\in \mathbb{N}\to n-1\in {\mathbb{N}}_0$$
16	14 15	sylbi	$$⊢\left(n\in {\mathbb{N}}_0\wedge \neg n=0\right)\to n-1\in {\mathbb{N}}_0$$
17		eqidd	$$⊢m=n-1\to 0=0$$
18		fconstmpt	$$⊢{\mathbb{N}}_0\times \left\{0\right\}=\left(m\in {\mathbb{N}}_0⟼0\right)$$
19	9 18	eqtri	$$⊢\mathrm{coeff}\left(0_{𝑝}\right)=\left(m\in {\mathbb{N}}_0⟼0\right)$$
20		c0ex	$$⊢0\in \mathrm{V}$$
21	17 19 20	fvmpt	$$⊢n-1\in {\mathbb{N}}_0\to \mathrm{coeff}\left(0_{𝑝}\right)\left(n-1\right)=0$$
22	16 21	syl	$$⊢\left(n\in {\mathbb{N}}_0\wedge \neg n=0\right)\to \mathrm{coeff}\left(0_{𝑝}\right)\left(n-1\right)=0$$
23	10 22	ifeqda	$$⊢n\in {\mathbb{N}}_0\to if\left(n=0,0,\mathrm{coeff}\left(0_{𝑝}\right)\left(n-1\right)\right)=0$$
24	23	mpteq2ia	$$⊢\left(n\in {\mathbb{N}}_0⟼if\left(n=0,0,\mathrm{coeff}\left(0_{𝑝}\right)\left(n-1\right)\right)\right)=\left(n\in {\mathbb{N}}_0⟼0\right)$$
25	8 9 24	3eqtr4ri	$$⊢\left(n\in {\mathbb{N}}_0⟼if\left(n=0,0,\mathrm{coeff}\left(0_{𝑝}\right)\left(n-1\right)\right)\right)=\mathrm{coeff}\left(0_{𝑝}\right)$$
26	7 25	eqtr4i	$$⊢\mathrm{coeff}\left(0_{𝑝}{\times }_f{X}^p\right)=\left(n\in {\mathbb{N}}_0⟼if\left(n=0,0,\mathrm{coeff}\left(0_{𝑝}\right)\left(n-1\right)\right)\right)$$
27		fvoveq1	$$⊢F=0_{𝑝}\to \mathrm{coeff}\left(F{\times }_f{X}^p\right)=\mathrm{coeff}\left(0_{𝑝}{\times }_f{X}^p\right)$$
28		simpl	$$⊢\left(F=0_{𝑝}\wedge n\in {\mathbb{N}}_0\right)\to F=0_{𝑝}$$
29	28	fveq2d	$$⊢\left(F=0_{𝑝}\wedge n\in {\mathbb{N}}_0\right)\to \mathrm{coeff}\left(F\right)=\mathrm{coeff}\left(0_{𝑝}\right)$$
30	29	fveq1d	$$⊢\left(F=0_{𝑝}\wedge n\in {\mathbb{N}}_0\right)\to \mathrm{coeff}\left(F\right)\left(n-1\right)=\mathrm{coeff}\left(0_{𝑝}\right)\left(n-1\right)$$
31	30	ifeq2d	$$⊢\left(F=0_{𝑝}\wedge n\in {\mathbb{N}}_0\right)\to if\left(n=0,0,\mathrm{coeff}\left(F\right)\left(n-1\right)\right)=if\left(n=0,0,\mathrm{coeff}\left(0_{𝑝}\right)\left(n-1\right)\right)$$
32	31	mpteq2dva	$$⊢F=0_{𝑝}\to \left(n\in {\mathbb{N}}_0⟼if\left(n=0,0,\mathrm{coeff}\left(F\right)\left(n-1\right)\right)\right)=\left(n\in {\mathbb{N}}_0⟼if\left(n=0,0,\mathrm{coeff}\left(0_{𝑝}\right)\left(n-1\right)\right)\right)$$
33	26 27 32	3eqtr4a	$$⊢F=0_{𝑝}\to \mathrm{coeff}\left(F{\times }_f{X}^p\right)=\left(n\in {\mathbb{N}}_0⟼if\left(n=0,0,\mathrm{coeff}\left(F\right)\left(n-1\right)\right)\right)$$
34	33	adantl	$$⊢\left(F\in \mathrm{Poly}\left(ℝ\right)\wedge F=0_{𝑝}\right)\to \mathrm{coeff}\left(F{\times }_f{X}^p\right)=\left(n\in {\mathbb{N}}_0⟼if\left(n=0,0,\mathrm{coeff}\left(F\right)\left(n-1\right)\right)\right)$$
35		simpl	$$⊢\left(F\in \mathrm{Poly}\left(ℝ\right)\wedge \neg F=0_{𝑝}\right)\to F\in \mathrm{Poly}\left(ℝ\right)$$
36		elsng	$$⊢F\in \mathrm{Poly}\left(ℝ\right)\to \left(F\in \left\{0_{𝑝}\right\}\leftrightarrow F=0_{𝑝}\right)$$
37	36	notbid	$$⊢F\in \mathrm{Poly}\left(ℝ\right)\to \left(\neg F\in \left\{0_{𝑝}\right\}\leftrightarrow \neg F=0_{𝑝}\right)$$
38	37	biimpar	$$⊢\left(F\in \mathrm{Poly}\left(ℝ\right)\wedge \neg F=0_{𝑝}\right)\to \neg F\in \left\{0_{𝑝}\right\}$$
39	35 38	eldifd	$$⊢\left(F\in \mathrm{Poly}\left(ℝ\right)\wedge \neg F=0_{𝑝}\right)\to F\in \left(\mathrm{Poly}\left(ℝ\right)\setminus \left\{0_{𝑝}\right\}\right)$$
40		plyn0mulidp	$$⊢F\in \left(\mathrm{Poly}\left(ℝ\right)\setminus \left\{0_{𝑝}\right\}\right)\to \mathrm{coeff}\left(F{\times }_f{X}^p\right)=\left(n\in {\mathbb{N}}_0⟼if\left(n=0,0,\mathrm{coeff}\left(F\right)\left(n-1\right)\right)\right)$$
41	39 40	syl	$$⊢\left(F\in \mathrm{Poly}\left(ℝ\right)\wedge \neg F=0_{𝑝}\right)\to \mathrm{coeff}\left(F{\times }_f{X}^p\right)=\left(n\in {\mathbb{N}}_0⟼if\left(n=0,0,\mathrm{coeff}\left(F\right)\left(n-1\right)\right)\right)$$
42	34 41	pm2.61dan	$$⊢F\in \mathrm{Poly}\left(ℝ\right)\to \mathrm{coeff}\left(F{\times }_f{X}^p\right)=\left(n\in {\mathbb{N}}_0⟼if\left(n=0,0,\mathrm{coeff}\left(F\right)\left(n-1\right)\right)\right)$$