plyf

Description: The polynomial is a function on the complex numbers. (Contributed by Mario Carneiro, 22-Jul-2014)

		Ref	Expression
	Assertion	plyf	$⊢ F \in Poly (S) \to F : ℂ ⟶ ℂ$

Proof

Step	Hyp	Ref	Expression
1		elply	$⊢ F \in Poly (S) \leftrightarrow (S \subseteq ℂ \land \exists n \in ℕ_{0} \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))$
2	1	simprbi	$⊢ F \in Poly (S) \to \exists n \in ℕ_{0} \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})$
3		fzfid	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land z \in ℂ) \to (0 \dots n) \in Fin$
4		plybss	$⊢ F \in Poly (S) \to S \subseteq ℂ$
5		0cnd	$⊢ F \in Poly (S) \to 0 \in ℂ$
6	5	snssd	$⊢ F \in Poly (S) \to \{0\} \subseteq ℂ$
7	4 6	unssd	$⊢ F \in Poly (S) \to S \cup \{0\} \subseteq ℂ$
8	7	ad2antrr	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land z \in ℂ) \to S \cup \{0\} \subseteq ℂ$
9	8	adantr	$⊢ (((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land z \in ℂ) \land k \in (0 \dots n)) \to S \cup \{0\} \subseteq ℂ$
10		simplrr	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land z \in ℂ) \to a \in ({(S \cup \{0\})}^{ℕ_{0}})$
11		cnex	$⊢ ℂ \in V$
12		ssexg	$⊢ (S \cup \{0\} \subseteq ℂ \land ℂ \in V) \to S \cup \{0\} \in V$
13	8 11 12	sylancl	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land z \in ℂ) \to S \cup \{0\} \in V$
14		nn0ex	$⊢ ℕ_{0} \in V$
15		elmapg	$⊢ (S \cup \{0\} \in V \land ℕ_{0} \in V) \to (a \in ({(S \cup \{0\})}^{ℕ_{0}}) \leftrightarrow a : ℕ_{0} ⟶ S \cup \{0\})$
16	13 14 15	sylancl	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land z \in ℂ) \to (a \in ({(S \cup \{0\})}^{ℕ_{0}}) \leftrightarrow a : ℕ_{0} ⟶ S \cup \{0\})$
17	10 16	mpbid	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land z \in ℂ) \to a : ℕ_{0} ⟶ S \cup \{0\}$
18		elfznn0	$⊢ k \in (0 \dots n) \to k \in ℕ_{0}$
19		ffvelrn	$⊢ (a : ℕ_{0} ⟶ S \cup \{0\} \land k \in ℕ_{0}) \to a (k) \in (S \cup \{0\})$
20	17 18 19	syl2an	$⊢ (((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land z \in ℂ) \land k \in (0 \dots n)) \to a (k) \in (S \cup \{0\})$
21	9 20	sseldd	$⊢ (((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land z \in ℂ) \land k \in (0 \dots n)) \to a (k) \in ℂ$
22		simpr	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land z \in ℂ) \to z \in ℂ$
23		expcl	$⊢ (z \in ℂ \land k \in ℕ_{0}) \to z^{k} \in ℂ$
24	22 18 23	syl2an	$⊢ (((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land z \in ℂ) \land k \in (0 \dots n)) \to z^{k} \in ℂ$
25	21 24	mulcld	$⊢ (((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land z \in ℂ) \land k \in (0 \dots n)) \to a (k) z^{k} \in ℂ$
26	3 25	fsumcl	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land z \in ℂ) \to \sum_{k = 0}^{n} a (k) z^{k} \in ℂ$
27	26	fmpttd	$⊢ (F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \to (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}) : ℂ ⟶ ℂ$
28		feq1	$⊢ F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}) \to (F : ℂ ⟶ ℂ \leftrightarrow (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}) : ℂ ⟶ ℂ)$
29	27 28	syl5ibrcom	$⊢ (F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \to (F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}) \to F : ℂ ⟶ ℂ)$
30	29	rexlimdvva	$⊢ F \in Poly (S) \to (\exists n \in ℕ_{0} \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}) \to F : ℂ ⟶ ℂ)$
31	2 30	mpd	$⊢ F \in Poly (S) \to F : ℂ ⟶ ℂ$

Metamath Proof Explorer

Theorem plyf

Proof