Theorem plyval

Description: Value of the polynomial set function. (Contributed by Mario Carneiro, 17-Jul-2014)

	Ref	Expression
Assertion	plyval	$$⊢S\subseteq ℂ\to \mathrm{Poly}\left(S\right)=\left\{f|\exists n\in {\mathbb{N}}_0\exists a\in \left({\left(S\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)f=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right\}$$

Proof

Step	Hyp	Ref	Expression
1		cnex	$$⊢ℂ\in \mathrm{V}$$
2	1	elpw2	$$⊢S\in 𝒫ℂ\leftrightarrow S\subseteq ℂ$$
3		uneq1	$$⊢x=S\to x\cup \left\{0\right\}=S\cup \left\{0\right\}$$
4	3	oveq1d	$$⊢x=S\to {\left(x\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}={\left(S\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}$$
5	4	rexeqdv	$$⊢x=S\to \left(\exists a\in \left({\left(x\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)f=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\leftrightarrow \exists a\in \left({\left(S\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)f=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)$$
6	5	rexbidv	$$⊢x=S\to \left(\exists n\in {\mathbb{N}}_0\exists a\in \left({\left(x\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)f=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\leftrightarrow \exists n\in {\mathbb{N}}_0\exists a\in \left({\left(S\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)f=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)$$
7	6	abbidv	$$⊢x=S\to \left\{f|\exists n\in {\mathbb{N}}_0\exists a\in \left({\left(x\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)f=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right\}=\left\{f|\exists n\in {\mathbb{N}}_0\exists a\in \left({\left(S\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)f=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right\}$$
8		df-ply	$$⊢\mathrm{Poly}=\left(x\in 𝒫ℂ⟼\left\{f|\exists n\in {\mathbb{N}}_0\exists a\in \left({\left(x\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)f=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right\}\right)$$
9		nn0ex	$$⊢{\mathbb{N}}_0\in \mathrm{V}$$
10		ovex	$$⊢{\left(S\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\in \mathrm{V}$$
11	9 10	ab2rexex	$$⊢\left\{f|\exists n\in {\mathbb{N}}_0\exists a\in \left({\left(S\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)f=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right\}\in \mathrm{V}$$
12	7 8 11	fvmpt	$$⊢S\in 𝒫ℂ\to \mathrm{Poly}\left(S\right)=\left\{f|\exists n\in {\mathbb{N}}_0\exists a\in \left({\left(S\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)f=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right\}$$
13	2 12	sylbir	$$⊢S\subseteq ℂ\to \mathrm{Poly}\left(S\right)=\left\{f|\exists n\in {\mathbb{N}}_0\exists a\in \left({\left(S\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)f=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right\}$$