Theorem plyeq0

Description: If a polynomial is zero at every point (or even just zero at the positive integers), then all the coefficients must be zero. This is the basis for the method of equating coefficients of equal polynomials, and ensures that df-coe is well-defined. (Contributed by Mario Carneiro, 22-Jul-2014)

	Ref	Expression
Hypotheses	plyeq0.1	$$⊢\phi \to S\subseteq ℂ$$
	plyeq0.2	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	plyeq0.3	$$⊢\phi \to A\in \left({\left(S\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)$$
	plyeq0.4	$$⊢\phi \to A\left[{\mathbb{Z}}_{\ge \left(N+1\right)}\right]=\left\{0\right\}$$
	plyeq0.5	$$⊢\phi \to 0_{𝑝}=\left(z\in ℂ⟼\sum _{k=0}^{N}A\left(k\right)z^k\right)$$
Assertion	plyeq0	$$⊢\phi \to A={\mathbb{N}}_0\times \left\{0\right\}$$

Proof

Step	Hyp	Ref	Expression
1		plyeq0.1	$$⊢\phi \to S\subseteq ℂ$$
2		plyeq0.2	$$⊢\phi \to N\in {\mathbb{N}}_0$$
3		plyeq0.3	$$⊢\phi \to A\in \left({\left(S\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)$$
4		plyeq0.4	$$⊢\phi \to A\left[{\mathbb{Z}}_{\ge \left(N+1\right)}\right]=\left\{0\right\}$$
5		plyeq0.5	$$⊢\phi \to 0_{𝑝}=\left(z\in ℂ⟼\sum _{k=0}^{N}A\left(k\right)z^k\right)$$
6		0cnd	$$⊢\phi \to 0\in ℂ$$
7	6	snssd	$$⊢\phi \to \left\{0\right\}\subseteq ℂ$$
8	1 7	unssd	$$⊢\phi \to S\cup \left\{0\right\}\subseteq ℂ$$
9		cnex	$$⊢ℂ\in \mathrm{V}$$
10		ssexg	$$⊢\left(S\cup \left\{0\right\}\subseteq ℂ\wedge ℂ\in \mathrm{V}\right)\to S\cup \left\{0\right\}\in \mathrm{V}$$
11	8 9 10	sylancl	$$⊢\phi \to S\cup \left\{0\right\}\in \mathrm{V}$$
12		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
13		elmapg	$$⊢\left(S\cup \left\{0\right\}\in \mathrm{V}\wedge {\mathbb{N}}_0\in \mathrm{V}\right)\to \left(A\in \left({\left(S\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)\leftrightarrow A:{\mathbb{N}}_0⟶S\cup \left\{0\right\}\right)$$
14	11 12 13	sylancl	$$⊢\phi \to \left(A\in \left({\left(S\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)\leftrightarrow A:{\mathbb{N}}_0⟶S\cup \left\{0\right\}\right)$$
15	3 14	mpbid	$$⊢\phi \to A:{\mathbb{N}}_0⟶S\cup \left\{0\right\}$$
16	15	ffnd	$$⊢\phi \to AFn{\mathbb{N}}_0$$
17		imadmrn	$$⊢A\left[\mathrm{dom}A\right]=\mathrm{ran}A$$
18		fdm	$$⊢A:{\mathbb{N}}_0⟶S\cup \left\{0\right\}\to \mathrm{dom}A={\mathbb{N}}_0$$
19		fimacnv	$$⊢A:{\mathbb{N}}_0⟶S\cup \left\{0\right\}\to A^{-1}\left[S\cup \left\{0\right\}\right]={\mathbb{N}}_0$$
20	18 19	eqtr4d	$$⊢A:{\mathbb{N}}_0⟶S\cup \left\{0\right\}\to \mathrm{dom}A=A^{-1}\left[S\cup \left\{0\right\}\right]$$
21	15 20	syl	$$⊢\phi \to \mathrm{dom}A=A^{-1}\left[S\cup \left\{0\right\}\right]$$
22		simpr	$$⊢\left(\phi \wedge A^{-1}\left[S\setminus \left\{0\right\}\right]=\varnothing \right)\to A^{-1}\left[S\setminus \left\{0\right\}\right]=\varnothing$$
23	1	adantr	$$⊢\left(\phi \wedge A^{-1}\left[S\setminus \left\{0\right\}\right]\ne \varnothing \right)\to S\subseteq ℂ$$
24	2	adantr	$$⊢\left(\phi \wedge A^{-1}\left[S\setminus \left\{0\right\}\right]\ne \varnothing \right)\to N\in {\mathbb{N}}_0$$
25	3	adantr	$$⊢\left(\phi \wedge A^{-1}\left[S\setminus \left\{0\right\}\right]\ne \varnothing \right)\to A\in \left({\left(S\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)$$
26	4	adantr	$$⊢\left(\phi \wedge A^{-1}\left[S\setminus \left\{0\right\}\right]\ne \varnothing \right)\to A\left[{\mathbb{Z}}_{\ge \left(N+1\right)}\right]=\left\{0\right\}$$
27	5	adantr	$$⊢\left(\phi \wedge A^{-1}\left[S\setminus \left\{0\right\}\right]\ne \varnothing \right)\to 0_{𝑝}=\left(z\in ℂ⟼\sum _{k=0}^{N}A\left(k\right)z^k\right)$$
28		eqid	$$⊢sup\left(A^{-1}\left[S\setminus \left\{0\right\}\right],ℝ,<\right)=sup\left(A^{-1}\left[S\setminus \left\{0\right\}\right],ℝ,<\right)$$
29		simpr	$$⊢\left(\phi \wedge A^{-1}\left[S\setminus \left\{0\right\}\right]\ne \varnothing \right)\to A^{-1}\left[S\setminus \left\{0\right\}\right]\ne \varnothing$$
30	23 24 25 26 27 28 29	plyeq0lem	$$⊢\neg \left(\phi \wedge A^{-1}\left[S\setminus \left\{0\right\}\right]\ne \varnothing \right)$$
31	30	pm2.21i	$$⊢\left(\phi \wedge A^{-1}\left[S\setminus \left\{0\right\}\right]\ne \varnothing \right)\to A^{-1}\left[S\setminus \left\{0\right\}\right]=\varnothing$$
32	22 31	pm2.61dane	$$⊢\phi \to A^{-1}\left[S\setminus \left\{0\right\}\right]=\varnothing$$
33	32	uneq1d	$$⊢\phi \to A^{-1}\left[S\setminus \left\{0\right\}\right]\cup A^{-1}\left[\left\{0\right\}\right]=\varnothing \cup A^{-1}\left[\left\{0\right\}\right]$$
34		undif1	$$⊢\left(S\setminus \left\{0\right\}\right)\cup \left\{0\right\}=S\cup \left\{0\right\}$$
35	34	imaeq2i	$$⊢A^{-1}\left[\left(S\setminus \left\{0\right\}\right)\cup \left\{0\right\}\right]=A^{-1}\left[S\cup \left\{0\right\}\right]$$
36		imaundi	$$⊢A^{-1}\left[\left(S\setminus \left\{0\right\}\right)\cup \left\{0\right\}\right]=A^{-1}\left[S\setminus \left\{0\right\}\right]\cup A^{-1}\left[\left\{0\right\}\right]$$
37	35 36	eqtr3i	$$⊢A^{-1}\left[S\cup \left\{0\right\}\right]=A^{-1}\left[S\setminus \left\{0\right\}\right]\cup A^{-1}\left[\left\{0\right\}\right]$$
38		un0	$$⊢A^{-1}\left[\left\{0\right\}\right]\cup \varnothing =A^{-1}\left[\left\{0\right\}\right]$$
39		uncom	$$⊢A^{-1}\left[\left\{0\right\}\right]\cup \varnothing =\varnothing \cup A^{-1}\left[\left\{0\right\}\right]$$
40	38 39	eqtr3i	$$⊢A^{-1}\left[\left\{0\right\}\right]=\varnothing \cup A^{-1}\left[\left\{0\right\}\right]$$
41	33 37 40	3eqtr4g	$$⊢\phi \to A^{-1}\left[S\cup \left\{0\right\}\right]=A^{-1}\left[\left\{0\right\}\right]$$
42	21 41	eqtrd	$$⊢\phi \to \mathrm{dom}A=A^{-1}\left[\left\{0\right\}\right]$$
43		eqimss	$$⊢\mathrm{dom}A=A^{-1}\left[\left\{0\right\}\right]\to \mathrm{dom}A\subseteq A^{-1}\left[\left\{0\right\}\right]$$
44	42 43	syl	$$⊢\phi \to \mathrm{dom}A\subseteq A^{-1}\left[\left\{0\right\}\right]$$
45	15	ffund	$$⊢\phi \to \mathrm{Fun}A$$
46		ssid	$$⊢\mathrm{dom}A\subseteq \mathrm{dom}A$$
47		funimass3	$$⊢\left(\mathrm{Fun}A\wedge \mathrm{dom}A\subseteq \mathrm{dom}A\right)\to \left(A\left[\mathrm{dom}A\right]\subseteq \left\{0\right\}\leftrightarrow \mathrm{dom}A\subseteq A^{-1}\left[\left\{0\right\}\right]\right)$$
48	45 46 47	sylancl	$$⊢\phi \to \left(A\left[\mathrm{dom}A\right]\subseteq \left\{0\right\}\leftrightarrow \mathrm{dom}A\subseteq A^{-1}\left[\left\{0\right\}\right]\right)$$
49	44 48	mpbird	$$⊢\phi \to A\left[\mathrm{dom}A\right]\subseteq \left\{0\right\}$$
50	17 49	eqsstrrid	$$⊢\phi \to \mathrm{ran}A\subseteq \left\{0\right\}$$
51		df-f	$$⊢A:{\mathbb{N}}_0⟶\left\{0\right\}\leftrightarrow \left(AFn{\mathbb{N}}_0\wedge \mathrm{ran}A\subseteq \left\{0\right\}\right)$$
52	16 50 51	sylanbrc	$$⊢\phi \to A:{\mathbb{N}}_0⟶\left\{0\right\}$$
53		c0ex	$$⊢0\in \mathrm{V}$$
54	53	fconst2	$$⊢A:{\mathbb{N}}_0⟶\left\{0\right\}\leftrightarrow A={\mathbb{N}}_0\times \left\{0\right\}$$
55	52 54	sylib	$$⊢\phi \to A={\mathbb{N}}_0\times \left\{0\right\}$$