Theorem elply

Description: Definition of a polynomial with coefficients in S . (Contributed by Mario Carneiro, 17-Jul-2014)

	Ref	Expression
Assertion	elply	$$⊢F\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)F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		plybss	$$⊢F\in \mathrm{Poly}\left(S\right)\to S\subseteq ℂ$$
2		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\}$$
3	2	eleq2d	$$⊢S\subseteq ℂ\to \left(F\in \mathrm{Poly}\left(S\right)\leftrightarrow F\in \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\}\right)$$
4		id	$$⊢F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\to F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)$$
5		cnex	$$⊢ℂ\in \mathrm{V}$$
6	5	mptex	$$⊢\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\in \mathrm{V}$$
7	4 6	eqeltrdi	$$⊢F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\to F\in \mathrm{V}$$
8	7	a1i	$$⊢\left(n\in {\mathbb{N}}_0\wedge a\in \left({\left(S\cup \left\{0\right\}\right)}^{{\mathbb{N}}_0}\right)\right)\to \left(F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\to F\in \mathrm{V}\right)$$
9	8	rexlimivv	$$⊢\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)\to F\in \mathrm{V}$$
10		eqeq1	$$⊢f=F\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)$$
11	10	2rexbidv	$$⊢f=F\to \left(\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)\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)$$
12	9 11	elab3	$$⊢F\in \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\}\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)$$
13	3 12	syl6bb	$$⊢S\subseteq ℂ\to \left(F\in \mathrm{Poly}\left(S\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)$$
14	1 13	biadanii	$$⊢F\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)F=\left(z\in ℂ⟼\sum _{k=0}^{n}a\left(k\right)z^k\right)\right)$$