Theorem elplyr

Description: Sufficient condition for elementhood in the set of polynomials. (Contributed by Mario Carneiro, 17-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

	Ref	Expression
Assertion	elplyr	$$⊢\left(S\subseteq ℂ\wedge N\in {\mathbb{N}}_0\wedge A:{\mathbb{N}}_0⟶S\right)\to \left(z\in ℂ⟼\sum _{k=0}^{N}A\left(k\right)z^k\right)\in \mathrm{Poly}\left(S\right)$$

Proof

Step	Hyp	Ref	Expression
1		simp1	$$⊢\left(S\subseteq ℂ\wedge N\in {\mathbb{N}}_0\wedge A:{\mathbb{N}}_0⟶S\right)\to S\subseteq ℂ$$
2		simp2	$$⊢\left(S\subseteq ℂ\wedge N\in {\mathbb{N}}_0\wedge A:{\mathbb{N}}_0⟶S\right)\to N\in {\mathbb{N}}_0$$
3		simp3	$$⊢\left(S\subseteq ℂ\wedge N\in {\mathbb{N}}_0\wedge A:{\mathbb{N}}_0⟶S\right)\to A:{\mathbb{N}}_0⟶S$$
4		ssun1	$$⊢S\subseteq S\cup \left\{0\right\}$$
5		fss	$$⊢\left(A:{\mathbb{N}}_0⟶S\wedge S\subseteq S\cup \left\{0\right\}\right)\to A:{\mathbb{N}}_0⟶S\cup \left\{0\right\}$$
6	3 4 5	sylancl	$$⊢\left(S\subseteq ℂ\wedge N\in {\mathbb{N}}_0\wedge A:{\mathbb{N}}_0⟶S\right)\to A:{\mathbb{N}}_0⟶S\cup \left\{0\right\}$$
7		0cnd	$$⊢\left(S\subseteq ℂ\wedge N\in {\mathbb{N}}_0\wedge A:{\mathbb{N}}_0⟶S\right)\to 0\in ℂ$$
8	7	snssd	$$⊢\left(S\subseteq ℂ\wedge N\in {\mathbb{N}}_0\wedge A:{\mathbb{N}}_0⟶S\right)\to \left\{0\right\}\subseteq ℂ$$
9	1 8	unssd	$$⊢\left(S\subseteq ℂ\wedge N\in {\mathbb{N}}_0\wedge A:{\mathbb{N}}_0⟶S\right)\to S\cup \left\{0\right\}\subseteq ℂ$$
10		cnex	$$⊢ℂ\in \mathrm{V}$$
11		ssexg	$$⊢\left(S\cup \left\{0\right\}\subseteq ℂ\wedge ℂ\in \mathrm{V}\right)\to S\cup \left\{0\right\}\in \mathrm{V}$$
12	9 10 11	sylancl	$$⊢\left(S\subseteq ℂ\wedge N\in {\mathbb{N}}_0\wedge A:{\mathbb{N}}_0⟶S\right)\to S\cup \left\{0\right\}\in \mathrm{V}$$
13		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
14		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)$$
15	12 13 14	sylancl	$$⊢\left(S\subseteq ℂ\wedge N\in {\mathbb{N}}_0\wedge A:{\mathbb{N}}_0⟶S\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)$$
16	6 15	mpbird	$$⊢\left(S\subseteq ℂ\wedge N\in {\mathbb{N}}_0\wedge A:{\mathbb{N}}_0⟶S\right)\to A\in \left({\left(S\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)$$
17		eqidd	$$⊢\left(S\subseteq ℂ\wedge N\in {\mathbb{N}}_0\wedge A:{\mathbb{N}}_0⟶S\right)\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)$$
18		oveq2	$$⊢n=N\to \left(0\dots n\right)=\left(0\dots N\right)$$
19	18	sumeq1d	$$⊢n=N\to \sum _{k=0}^{n}a\left(k\right)z^k=\sum _{k=0}^{N}a\left(k\right)z^k$$
20	19	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)$$
21	20	eqeq2d	$$⊢n=N\to \left(\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)\leftrightarrow \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)\right)$$
22		fveq1	$$⊢a=A\to a\left(k\right)=A\left(k\right)$$
23	22	oveq1d	$$⊢a=A\to a\left(k\right)z^k=A\left(k\right)z^k$$
24	23	sumeq2sdv	$$⊢a=A\to \sum _{k=0}^{N}a\left(k\right)z^k=\sum _{k=0}^{N}A\left(k\right)z^k$$
25	24	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)$$
26	25	eqeq2d	$$⊢a=A\to \left(\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)\leftrightarrow \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)\right)$$
27	21 26	rspc2ev	$$⊢\left(N\in {\mathbb{N}}_0\wedge A\in \left({\left(S\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)\wedge \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)\right)\to \exists n\in {\mathbb{N}}_0\exists a\in \left({\left(S\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)\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)$$
28	2 16 17 27	syl3anc	$$⊢\left(S\subseteq ℂ\wedge N\in {\mathbb{N}}_0\wedge A:{\mathbb{N}}_0⟶S\right)\to \exists n\in {\mathbb{N}}_0\exists a\in \left({\left(S\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)\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)$$
29		elply	$$⊢\left(z\in ℂ⟼\sum _{k=0}^{N}A\left(k\right)z^k\right)\in \mathrm{Poly}\left(S\right)\leftrightarrow \left(S\subseteq ℂ\wedge \exists n\in {\mathbb{N}}_0\exists a\in \left({\left(S\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)\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)\right)$$
30	1 28 29	sylanbrc	$$⊢\left(S\subseteq ℂ\wedge N\in {\mathbb{N}}_0\wedge A:{\mathbb{N}}_0⟶S\right)\to \left(z\in ℂ⟼\sum _{k=0}^{N}A\left(k\right)z^k\right)\in \mathrm{Poly}\left(S\right)$$