coeid

Description: Reconstruct a polynomial as an explicit sum of the coefficient function up to the degree of the polynomial. (Contributed by Mario Carneiro, 22-Jul-2014)

	Ref	Expression
Hypotheses	dgrub.1	$⊢ A = coeff (F)$
	dgrub.2	$⊢ N = \deg (F)$
Assertion	coeid	$⊢ F \in Poly (S) \to F = (z \in ℂ ⟼ \sum_{k = 0}^{N} A (k) z^{k})$

Proof

Step	Hyp	Ref	Expression
1		dgrub.1	$⊢ A = coeff (F)$
2		dgrub.2	$⊢ N = \deg (F)$
3		elply2	$⊢ F \in Poly (S) \leftrightarrow (S \subseteq ℂ \land \exists n \in ℕ_{0} \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (x \in ℂ ⟼ \sum_{m = 0}^{n} a (m) x^{m})))$
4	3	simprbi	$⊢ F \in Poly (S) \to \exists n \in ℕ_{0} \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (x \in ℂ ⟼ \sum_{m = 0}^{n} a (m) x^{m}))$
5		simpll	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (x \in ℂ ⟼ \sum_{m = 0}^{n} a (m) x^{m}))) \to F \in Poly (S)$
6		simplrl	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (x \in ℂ ⟼ \sum_{m = 0}^{n} a (m) x^{m}))) \to n \in ℕ_{0}$
7		simplrr	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (x \in ℂ ⟼ \sum_{m = 0}^{n} a (m) x^{m}))) \to a \in ({(S \cup \{0\})}^{ℕ_{0}})$
8		simprl	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (x \in ℂ ⟼ \sum_{m = 0}^{n} a (m) x^{m}))) \to a [ℤ_{\geq (n + 1)}] = \{0\}$
9		simprr	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (x \in ℂ ⟼ \sum_{m = 0}^{n} a (m) x^{m}))) \to F = (x \in ℂ ⟼ \sum_{m = 0}^{n} a (m) x^{m})$
10		fveq2	$⊢ m = k \to a (m) = a (k)$
11		oveq2	$⊢ m = k \to x^{m} = x^{k}$
12	10 11	oveq12d	$⊢ m = k \to a (m) x^{m} = a (k) x^{k}$
13	12	cbvsumv	$⊢ \sum_{m = 0}^{n} a (m) x^{m} = \sum_{k = 0}^{n} a (k) x^{k}$
14		oveq1	$⊢ x = z \to x^{k} = z^{k}$
15	14	oveq2d	$⊢ x = z \to a (k) x^{k} = a (k) z^{k}$
16	15	sumeq2sdv	$⊢ x = z \to \sum_{k = 0}^{n} a (k) x^{k} = \sum_{k = 0}^{n} a (k) z^{k}$
17	13 16	syl5eq	$⊢ x = z \to \sum_{m = 0}^{n} a (m) x^{m} = \sum_{k = 0}^{n} a (k) z^{k}$
18	17	cbvmptv	$⊢ (x \in ℂ ⟼ \sum_{m = 0}^{n} a (m) x^{m}) = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})$
19	9 18	syl6eq	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (x \in ℂ ⟼ \sum_{m = 0}^{n} a (m) x^{m}))) \to F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})$
20	1 2 5 6 7 8 19	coeidlem	$⊢ ((F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \land (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (x \in ℂ ⟼ \sum_{m = 0}^{n} a (m) x^{m}))) \to F = (z \in ℂ ⟼ \sum_{k = 0}^{N} A (k) z^{k})$
21	20	ex	$⊢ (F \in Poly (S) \land (n \in ℕ_{0} \land a \in ({(S \cup \{0\})}^{ℕ_{0}}))) \to ((a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (x \in ℂ ⟼ \sum_{m = 0}^{n} a (m) x^{m})) \to F = (z \in ℂ ⟼ \sum_{k = 0}^{N} A (k) z^{k}))$
22	21	rexlimdvva	$⊢ F \in Poly (S) \to (\exists n \in ℕ_{0} \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (x \in ℂ ⟼ \sum_{m = 0}^{n} a (m) x^{m})) \to F = (z \in ℂ ⟼ \sum_{k = 0}^{N} A (k) z^{k}))$
23	4 22	mpd	$⊢ F \in Poly (S) \to F = (z \in ℂ ⟼ \sum_{k = 0}^{N} A (k) z^{k})$

Metamath Proof Explorer

Theorem coeid

Proof