plyn0mulidp

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

		Ref	Expression
	Assertion	plyn0mulidp	$⊢ F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \to coeff (F \times_{f} X^{p}) = (n \in ℕ_{0} ⟼ if (n = 0, 0, coeff (F) (n - 1)))$

Proof

Step	Hyp	Ref	Expression
1		eldifi	$⊢ F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \to F \in Poly (ℝ)$
2		ax-resscn	$⊢ ℝ \subseteq ℂ$
3		1re	$⊢ 1 \in ℝ$
4		plyid	$⊢ (ℝ \subseteq ℂ \land 1 \in ℝ) \to X^{p} \in Poly (ℝ)$
5	2 3 4	mp2an	$⊢ X^{p} \in Poly (ℝ)$
6	5	a1i	$⊢ F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \to X^{p} \in Poly (ℝ)$
7		simprl	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land (x \in ℝ \land y \in ℝ)) \to x \in ℝ$
8		simprr	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land (x \in ℝ \land y \in ℝ)) \to y \in ℝ$
9	7 8	readdcld	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land (x \in ℝ \land y \in ℝ)) \to x + y \in ℝ$
10	7 8	remulcld	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land (x \in ℝ \land y \in ℝ)) \to x y \in ℝ$
11	1 6 9 10	plymul	$⊢ F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \to F \times_{f} X^{p} \in Poly (ℝ)$
12		0re	$⊢ 0 \in ℝ$
13		eqid	$⊢ coeff (F \times_{f} X^{p}) = coeff (F \times_{f} X^{p})$
14	13	coef2	$⊢ (F \times_{f} X^{p} \in Poly (ℝ) \land 0 \in ℝ) \to coeff (F \times_{f} X^{p}) : ℕ_{0} ⟶ ℝ$
15	11 12 14	sylancl	$⊢ F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \to coeff (F \times_{f} X^{p}) : ℕ_{0} ⟶ ℝ$
16	15	feqmptd	$⊢ F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \to coeff (F \times_{f} X^{p}) = (n \in ℕ_{0} ⟼ coeff (F \times_{f} X^{p}) (n))$
17		cnex	$⊢ ℂ \in V$
18	17	a1i	$⊢ F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \to ℂ \in V$
19		plyf	$⊢ F \in Poly (ℝ) \to F : ℂ ⟶ ℂ$
20	1 19	syl	$⊢ F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \to F : ℂ ⟶ ℂ$
21		plyf	$⊢ X^{p} \in Poly (ℝ) \to X^{p} : ℂ ⟶ ℂ$
22	5 21	ax-mp	$⊢ X^{p} : ℂ ⟶ ℂ$
23	22	a1i	$⊢ F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \to X^{p} : ℂ ⟶ ℂ$
24		simprl	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land (x \in ℂ \land y \in ℂ)) \to x \in ℂ$
25		simprr	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land (x \in ℂ \land y \in ℂ)) \to y \in ℂ$
26	24 25	mulcomd	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land (x \in ℂ \land y \in ℂ)) \to x y = y x$
27	18 20 23 26	caofcom	$⊢ F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \to F \times_{f} X^{p} = X^{p} \times_{f} F$
28	27	fveq2d	$⊢ F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \to coeff (F \times_{f} X^{p}) = coeff (X^{p} \times_{f} F)$
29	28	fveq1d	$⊢ F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \to coeff (F \times_{f} X^{p}) (n) = coeff (X^{p} \times_{f} F) (n)$
30	29	adantr	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \to coeff (F \times_{f} X^{p}) (n) = coeff (X^{p} \times_{f} F) (n)$
31	5	a1i	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \to X^{p} \in Poly (ℝ)$
32	1	adantr	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \to F \in Poly (ℝ)$
33		simpr	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \to n \in ℕ_{0}$
34		eqid	$⊢ coeff (X^{p}) = coeff (X^{p})$
35		eqid	$⊢ coeff (F) = coeff (F)$
36	34 35	coemul	$⊢ (X^{p} \in Poly (ℝ) \land F \in Poly (ℝ) \land n \in ℕ_{0}) \to coeff (X^{p} \times_{f} F) (n) = \sum_{i = 0}^{n} coeff (X^{p}) (i) coeff (F) (n - i)$
37	31 32 33 36	syl3anc	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \to coeff (X^{p} \times_{f} F) (n) = \sum_{i = 0}^{n} coeff (X^{p}) (i) coeff (F) (n - i)$
38		elfznn0	$⊢ i \in (0 \dots n) \to i \in ℕ_{0}$
39		coeidp	$⊢ i \in ℕ_{0} \to coeff (X^{p}) (i) = if (i = 1, 1, 0)$
40	38 39	syl	$⊢ i \in (0 \dots n) \to coeff (X^{p}) (i) = if (i = 1, 1, 0)$
41	40	oveq1d	$⊢ i \in (0 \dots n) \to coeff (X^{p}) (i) coeff (F) (n - i) = if (i = 1, 1, 0) coeff (F) (n - i)$
42		ovif	$⊢ if (i = 1, 1, 0) coeff (F) (n - i) = if (i = 1, 1 coeff (F) (n - i), 0 \cdot coeff (F) (n - i))$
43	41 42	eqtrdi	$⊢ i \in (0 \dots n) \to coeff (X^{p}) (i) coeff (F) (n - i) = if (i = 1, 1 coeff (F) (n - i), 0 \cdot coeff (F) (n - i))$
44	43	adantl	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \land i \in (0 \dots n)) \to coeff (X^{p}) (i) coeff (F) (n - i) = if (i = 1, 1 coeff (F) (n - i), 0 \cdot coeff (F) (n - i))$
45	44	sumeq2dv	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \to \sum_{i = 0}^{n} coeff (X^{p}) (i) coeff (F) (n - i) = \sum_{i = 0}^{n} if (i = 1, 1 coeff (F) (n - i), 0 \cdot coeff (F) (n - i))$
46		velsn	$⊢ i \in \{1\} \leftrightarrow i = 1$
47	46	bicomi	$⊢ i = 1 \leftrightarrow i \in \{1\}$
48	47	a1i	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \land i \in (0 \dots n)) \to (i = 1 \leftrightarrow i \in \{1\})$
49	35	coef2	$⊢ (F \in Poly (ℝ) \land 0 \in ℝ) \to coeff (F) : ℕ_{0} ⟶ ℝ$
50	1 12 49	sylancl	$⊢ F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \to coeff (F) : ℕ_{0} ⟶ ℝ$
51	50	ad2antrr	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \land i \in (0 \dots n)) \to coeff (F) : ℕ_{0} ⟶ ℝ$
52		fznn0sub	$⊢ i \in (0 \dots n) \to n - i \in ℕ_{0}$
53	52	adantl	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \land i \in (0 \dots n)) \to n - i \in ℕ_{0}$
54	51 53	ffvelcdmd	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \land i \in (0 \dots n)) \to coeff (F) (n - i) \in ℝ$
55	54	recnd	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \land i \in (0 \dots n)) \to coeff (F) (n - i) \in ℂ$
56	55	mullidd	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \land i \in (0 \dots n)) \to 1 coeff (F) (n - i) = coeff (F) (n - i)$
57	55	mul02d	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \land i \in (0 \dots n)) \to 0 \cdot coeff (F) (n - i) = 0$
58	48 56 57	ifbieq12d	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \land i \in (0 \dots n)) \to if (i = 1, 1 coeff (F) (n - i), 0 \cdot coeff (F) (n - i)) = if (i \in \{1\}, coeff (F) (n - i), 0)$
59	58	sumeq2dv	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \to \sum_{i = 0}^{n} if (i = 1, 1 coeff (F) (n - i), 0 \cdot coeff (F) (n - i)) = \sum_{i = 0}^{n} if (i \in \{1\}, coeff (F) (n - i), 0)$
60		eqeq2	$⊢ 0 = if (n = 0, 0, coeff (F) (n - 1)) \to (\sum_{i = 0}^{n} if (i \in \{1\}, coeff (F) (n - i), 0) = 0 \leftrightarrow \sum_{i = 0}^{n} if (i \in \{1\}, coeff (F) (n - i), 0) = if (n = 0, 0, coeff (F) (n - 1)))$
61		eqeq2	$⊢ coeff (F) (n - 1) = if (n = 0, 0, coeff (F) (n - 1)) \to (\sum_{i = 0}^{n} if (i \in \{1\}, coeff (F) (n - i), 0) = coeff (F) (n - 1) \leftrightarrow \sum_{i = 0}^{n} if (i \in \{1\}, coeff (F) (n - i), 0) = if (n = 0, 0, coeff (F) (n - 1)))$
62		oveq2	$⊢ n = 0 \to (0 \dots n) = (0 \dots 0)$
63		0z	$⊢ 0 \in ℤ$
64		fzsn	$⊢ 0 \in ℤ \to (0 \dots 0) = \{0\}$
65	63 64	ax-mp	$⊢ (0 \dots 0) = \{0\}$
66	62 65	eqtrdi	$⊢ n = 0 \to (0 \dots n) = \{0\}$
67		elsni	$⊢ i \in \{0\} \to i = 0$
68	67	adantl	$⊢ (n = 0 \land i \in \{0\}) \to i = 0$
69		ax-1ne0	$⊢ 1 \neq 0$
70	69	nesymi	$⊢ \neg 0 = 1$
71		eqeq1	$⊢ i = 0 \to (i = 1 \leftrightarrow 0 = 1)$
72	70 71	mtbiri	$⊢ i = 0 \to \neg i = 1$
73	47	notbii	$⊢ \neg i = 1 \leftrightarrow \neg i \in \{1\}$
74	73	biimpi	$⊢ \neg i = 1 \to \neg i \in \{1\}$
75		iffalse	$⊢ \neg i \in \{1\} \to if (i \in \{1\}, coeff (F) (n - i), 0) = 0$
76	68 72 74 75	4syl	$⊢ (n = 0 \land i \in \{0\}) \to if (i \in \{1\}, coeff (F) (n - i), 0) = 0$
77	66 76	sumeq12rdv	$⊢ n = 0 \to \sum_{i = 0}^{n} if (i \in \{1\}, coeff (F) (n - i), 0) = \sum_{i \in \{0\}} 0$
78		snfi	$⊢ \{0\} \in Fin$
79	78	olci	$⊢ (\{0\} \subseteq ℤ_{\geq 0} \lor \{0\} \in Fin)$
80		sumz	$⊢ (\{0\} \subseteq ℤ_{\geq 0} \lor \{0\} \in Fin) \to \sum_{i \in \{0\}} 0 = 0$
81	79 80	ax-mp	$⊢ \sum_{i \in \{0\}} 0 = 0$
82	77 81	eqtrdi	$⊢ n = 0 \to \sum_{i = 0}^{n} if (i \in \{1\}, coeff (F) (n - i), 0) = 0$
83	82	adantl	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \land n = 0) \to \sum_{i = 0}^{n} if (i \in \{1\}, coeff (F) (n - i), 0) = 0$
84		simpll	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \land \neg n = 0) \to F \in (Poly (ℝ) ∖ \{0_{𝑝}\})$
85	33	adantr	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \land \neg n = 0) \to n \in ℕ_{0}$
86		simpr	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \land \neg n = 0) \to \neg n = 0$
87	86	neqned	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \land \neg n = 0) \to n \neq 0$
88		elnnne0	$⊢ n \in ℕ \leftrightarrow (n \in ℕ_{0} \land n \neq 0)$
89	85 87 88	sylanbrc	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \land \neg n = 0) \to n \in ℕ$
90		1nn0	$⊢ 1 \in ℕ_{0}$
91	90	a1i	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \to 1 \in ℕ_{0}$
92		simpr	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \to n \in ℕ$
93	92	nnnn0d	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \to n \in ℕ_{0}$
94	92	nnge1d	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \to 1 \leq n$
95		elfz2nn0	$⊢ 1 \in (0 \dots n) \leftrightarrow (1 \in ℕ_{0} \land n \in ℕ_{0} \land 1 \leq n)$
96	91 93 94 95	syl3anbrc	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \to 1 \in (0 \dots n)$
97	96	snssd	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \to \{1\} \subseteq (0 \dots n)$
98	50	ad2antrr	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \land i \in \{1\}) \to coeff (F) : ℕ_{0} ⟶ ℝ$
99		oveq2	$⊢ i = 1 \to n - i = n - 1$
100	46 99	sylbi	$⊢ i \in \{1\} \to n - i = n - 1$
101	100	adantl	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \land i \in \{1\}) \to n - i = n - 1$
102		nnm1nn0	$⊢ n \in ℕ \to n - 1 \in ℕ_{0}$
103	102	ad2antlr	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \land i \in \{1\}) \to n - 1 \in ℕ_{0}$
104	101 103	eqeltrd	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \land i \in \{1\}) \to n - i \in ℕ_{0}$
105	98 104	ffvelcdmd	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \land i \in \{1\}) \to coeff (F) (n - i) \in ℝ$
106	105	recnd	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \land i \in \{1\}) \to coeff (F) (n - i) \in ℂ$
107	106	ralrimiva	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \to \forall i \in \{1\} coeff (F) (n - i) \in ℂ$
108		fzfi	$⊢ (0 \dots n) \in Fin$
109	108	olci	$⊢ ((0 \dots n) \subseteq ℤ_{\geq 0} \lor (0 \dots n) \in Fin)$
110	109	a1i	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \to ((0 \dots n) \subseteq ℤ_{\geq 0} \lor (0 \dots n) \in Fin)$
111		sumss2	$⊢ ((\{1\} \subseteq (0 \dots n) \land \forall i \in \{1\} coeff (F) (n - i) \in ℂ) \land ((0 \dots n) \subseteq ℤ_{\geq 0} \lor (0 \dots n) \in Fin)) \to \sum_{i \in \{1\}} coeff (F) (n - i) = \sum_{i = 0}^{n} if (i \in \{1\}, coeff (F) (n - i), 0)$
112	97 107 110 111	syl21anc	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \to \sum_{i \in \{1\}} coeff (F) (n - i) = \sum_{i = 0}^{n} if (i \in \{1\}, coeff (F) (n - i), 0)$
113	50	adantr	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \to coeff (F) : ℕ_{0} ⟶ ℝ$
114	102	adantl	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \to n - 1 \in ℕ_{0}$
115	113 114	ffvelcdmd	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \to coeff (F) (n - 1) \in ℝ$
116	115	recnd	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \to coeff (F) (n - 1) \in ℂ$
117	99	fveq2d	$⊢ i = 1 \to coeff (F) (n - i) = coeff (F) (n - 1)$
118	117	sumsn	$⊢ (1 \in ℝ \land coeff (F) (n - 1) \in ℂ) \to \sum_{i \in \{1\}} coeff (F) (n - i) = coeff (F) (n - 1)$
119	3 116 118	sylancr	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \to \sum_{i \in \{1\}} coeff (F) (n - i) = coeff (F) (n - 1)$
120	112 119	eqtr3d	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ) \to \sum_{i = 0}^{n} if (i \in \{1\}, coeff (F) (n - i), 0) = coeff (F) (n - 1)$
121	84 89 120	syl2anc	$⊢ ((F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \land \neg n = 0) \to \sum_{i = 0}^{n} if (i \in \{1\}, coeff (F) (n - i), 0) = coeff (F) (n - 1)$
122	60 61 83 121	ifbothda	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \to \sum_{i = 0}^{n} if (i \in \{1\}, coeff (F) (n - i), 0) = if (n = 0, 0, coeff (F) (n - 1))$
123	59 122	eqtrd	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \to \sum_{i = 0}^{n} if (i = 1, 1 coeff (F) (n - i), 0 \cdot coeff (F) (n - i)) = if (n = 0, 0, coeff (F) (n - 1))$
124	37 45 123	3eqtrd	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \to coeff (X^{p} \times_{f} F) (n) = if (n = 0, 0, coeff (F) (n - 1))$
125	30 124	eqtrd	$⊢ (F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \land n \in ℕ_{0}) \to coeff (F \times_{f} X^{p}) (n) = if (n = 0, 0, coeff (F) (n - 1))$
126	125	mpteq2dva	$⊢ F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \to (n \in ℕ_{0} ⟼ coeff (F \times_{f} X^{p}) (n)) = (n \in ℕ_{0} ⟼ if (n = 0, 0, coeff (F) (n - 1)))$
127	16 126	eqtrd	$⊢ F \in (Poly (ℝ) ∖ \{0_{𝑝}\}) \to coeff (F \times_{f} X^{p}) = (n \in ℕ_{0} ⟼ if (n = 0, 0, coeff (F) (n - 1)))$

Metamath Proof Explorer

Theorem plyn0mulidp

Proof