Theorem coeeq

Description: If A satisfies the properties of the coefficient function, it must be equal to the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

	Ref	Expression
Hypotheses	coeeq.1	$$⊢\phi \to F\in \mathrm{Poly}\left(S\right)$$
	coeeq.2	$$⊢\phi \to N\in {\mathbb{N}}_0$$
	coeeq.3	$$⊢\phi \to A:{\mathbb{N}}_0⟶ℂ$$
	coeeq.4	$$⊢\phi \to A\left[{\mathbb{Z}}_{\ge \left(N+1\right)}\right]=\left\{0\right\}$$
	coeeq.5	$$⊢\phi \to F=\left(z\in ℂ⟼\sum _{k=0}^{N}A\left(k\right)z^k\right)$$
Assertion	coeeq	$$⊢\phi \to \mathrm{coeff}\left(F\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		coeeq.1	$$⊢\phi \to F\in \mathrm{Poly}\left(S\right)$$
2		coeeq.2	$$⊢\phi \to N\in {\mathbb{N}}_0$$
3		coeeq.3	$$⊢\phi \to A:{\mathbb{N}}_0⟶ℂ$$
4		coeeq.4	$$⊢\phi \to A\left[{\mathbb{Z}}_{\ge \left(N+1\right)}\right]=\left\{0\right\}$$
5		coeeq.5	$$⊢\phi \to F=\left(z\in ℂ⟼\sum _{k=0}^{N}A\left(k\right)z^k\right)$$
6		coeval	$$⊢F\in \mathrm{Poly}\left(S\right)\to \mathrm{coeff}\left(F\right)=\left(\iota a\in \left({ℂ}^{{\mathbb{N}}_0}\right)|\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\right)$$
7	1 6	syl	$$⊢\phi \to \mathrm{coeff}\left(F\right)=\left(\iota a\in \left({ℂ}^{{\mathbb{N}}_0}\right)|\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\right)$$
8		fvoveq1	$$⊢n=N\to {\mathbb{Z}}_{\ge \left(n+1\right)}={\mathbb{Z}}_{\ge \left(N+1\right)}$$
9	8	imaeq2d	$$⊢n=N\to A\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=A\left[{\mathbb{Z}}_{\ge \left(N+1\right)}\right]$$
10	9	eqeq1d	$$⊢n=N\to \left(A\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\leftrightarrow A\left[{\mathbb{Z}}_{\ge \left(N+1\right)}\right]=\left\{0\right\}\right)$$
11		oveq2	$$⊢n=N\to \left(0\dots n\right)=\left(0\dots N\right)$$
12	11	sumeq1d	$$⊢n=N\to \sum _{k=0}^{n}A\left(k\right)z^k=\sum _{k=0}^{N}A\left(k\right)z^k$$
13	12	mpteq2dv	$$⊢n=N\to \left(z\in ℂ⟼\sum _{k=0}^{n}A\left(k\right)z^k\right)=\left(z\in ℂ⟼\sum _{k=0}^{N}A\left(k\right)z^k\right)$$
14	13	eqeq2d	$$⊢n=N\to \left(F=\left(z\in ℂ⟼\sum _{k=0}^{n}A\left(k\right)z^k\right)\leftrightarrow F=\left(z\in ℂ⟼\sum _{k=0}^{N}A\left(k\right)z^k\right)\right)$$
15	10 14	anbi12d	$$⊢n=N\to \left(\left(A\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}A\left(k\right)z^k\right)\right)\leftrightarrow \left(A\left[{\mathbb{Z}}_{\ge \left(N+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{N}A\left(k\right)z^k\right)\right)\right)$$
16	15	rspcev	$$⊢\left(N\in {\mathbb{N}}_0\wedge \left(A\left[{\mathbb{Z}}_{\ge \left(N+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{N}A\left(k\right)z^k\right)\right)\right)\to \exists n\in {\mathbb{N}}_0\left(A\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}A\left(k\right)z^k\right)\right)$$
17	2 4 5 16	syl12anc	$$⊢\phi \to \exists n\in {\mathbb{N}}_0\left(A\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}A\left(k\right)z^k\right)\right)$$
18		cnex	$$⊢ℂ\in \mathrm{V}$$
19		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
20	18 19	elmap	$$⊢A\in \left({ℂ}^{{\mathbb{N}}_0}\right)\leftrightarrow A:{\mathbb{N}}_0⟶ℂ$$
21	3 20	sylibr	$$⊢\phi \to A\in \left({ℂ}^{{\mathbb{N}}_0}\right)$$
22		coeeu	$$⊢F\in \mathrm{Poly}\left(S\right)\to \exists !a\in \left({ℂ}^{{\mathbb{N}}_0}\right)\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)$$
23	1 22	syl	$$⊢\phi \to \exists !a\in \left({ℂ}^{{\mathbb{N}}_0}\right)\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)$$
24		imaeq1	$$⊢a=A\to a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=A\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]$$
25	24	eqeq1d	$$⊢a=A\to \left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\leftrightarrow A\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\right)$$
26		fveq1	$$⊢a=A\to a\left(k\right)=A\left(k\right)$$
27	26	oveq1d	$$⊢a=A\to a\left(k\right)z^k=A\left(k\right)z^k$$
28	27	sumeq2sdv	$$⊢a=A\to \sum _{k=0}^{n}a\left(k\right)z^k=\sum _{k=0}^{n}A\left(k\right)z^k$$
29	28	mpteq2dv	$$⊢a=A\to \left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)=\left(z\in ℂ⟼\sum _{k=0}^{n}A\left(k\right)z^k\right)$$
30	29	eqeq2d	$$⊢a=A\to \left(F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\leftrightarrow F=\left(z\in ℂ⟼\sum _{k=0}^{n}A\left(k\right)z^k\right)\right)$$
31	25 30	anbi12d	$$⊢a=A\to \left(\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\leftrightarrow \left(A\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}A\left(k\right)z^k\right)\right)\right)$$
32	31	rexbidv	$$⊢a=A\to \left(\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\leftrightarrow \exists n\in {\mathbb{N}}_0\left(A\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}A\left(k\right)z^k\right)\right)\right)$$
33	32	riota2	$$⊢\left(A\in \left({ℂ}^{{\mathbb{N}}_0}\right)\wedge \exists !a\in \left({ℂ}^{{\mathbb{N}}_0}\right)\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\right)\to \left(\exists n\in {\mathbb{N}}_0\left(A\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}A\left(k\right)z^k\right)\right)\leftrightarrow \left(\iota a\in \left({ℂ}^{{\mathbb{N}}_0}\right)|\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\right)=A\right)$$
34	21 23 33	syl2anc	$$⊢\phi \to \left(\exists n\in {\mathbb{N}}_0\left(A\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}A\left(k\right)z^k\right)\right)\leftrightarrow \left(\iota a\in \left({ℂ}^{{\mathbb{N}}_0}\right)|\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\right)=A\right)$$
35	17 34	mpbid	$$⊢\phi \to \left(\iota a\in \left({ℂ}^{{\mathbb{N}}_0}\right)|\exists n\in {\mathbb{N}}_0\left(a\left[{\mathbb{Z}}_{\ge \left(n+1\right)}\right]=\left\{0\right\}\wedge F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)\right)=A$$
36	7 35	eqtrd	$$⊢\phi \to \mathrm{coeff}\left(F\right)=A$$