coeeu

Description: Uniqueness of the coefficient function. (Contributed by Mario Carneiro, 22-Jul-2014) (Revised by Mario Carneiro, 23-Aug-2014)

		Ref	Expression
	Assertion	coeeu	$⊢ F \in Poly (S) \to \exists! a \in (ℂ^{ℕ_{0}}) \exists n \in ℕ_{0} (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))$

Proof

Step	Hyp	Ref	Expression
1		plyssc	$⊢ Poly (S) \subseteq Poly (ℂ)$
2	1	sseli	$⊢ F \in Poly (S) \to F \in Poly (ℂ)$
3		elply2	$⊢ F \in Poly (ℂ) \leftrightarrow (ℂ \subseteq ℂ \land \exists n \in ℕ_{0} \exists a \in ({(ℂ \cup \{0\})}^{ℕ_{0}}) (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})))$
4	3	simprbi	$⊢ F \in Poly (ℂ) \to \exists n \in ℕ_{0} \exists a \in ({(ℂ \cup \{0\})}^{ℕ_{0}}) (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))$
5		rexcom	$⊢ \exists n \in ℕ_{0} \exists a \in ({(ℂ \cup \{0\})}^{ℕ_{0}}) (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \leftrightarrow \exists a \in ({(ℂ \cup \{0\})}^{ℕ_{0}}) \exists n \in ℕ_{0} (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))$
6	4 5	sylib	$⊢ F \in Poly (ℂ) \to \exists a \in ({(ℂ \cup \{0\})}^{ℕ_{0}}) \exists n \in ℕ_{0} (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))$
7	2 6	syl	$⊢ F \in Poly (S) \to \exists a \in ({(ℂ \cup \{0\})}^{ℕ_{0}}) \exists n \in ℕ_{0} (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))$
8		0cn	$⊢ 0 \in ℂ$
9		snssi	$⊢ 0 \in ℂ \to \{0\} \subseteq ℂ$
10	8 9	ax-mp	$⊢ \{0\} \subseteq ℂ$
11		ssequn2	$⊢ \{0\} \subseteq ℂ \leftrightarrow ℂ \cup \{0\} = ℂ$
12	10 11	mpbi	$⊢ ℂ \cup \{0\} = ℂ$
13	12	oveq1i	$⊢ {(ℂ \cup \{0\})}^{ℕ_{0}} = ℂ^{ℕ_{0}}$
14	13	rexeqi	$⊢ \exists a \in ({(ℂ \cup \{0\})}^{ℕ_{0}}) \exists n \in ℕ_{0} (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \leftrightarrow \exists a \in (ℂ^{ℕ_{0}}) \exists n \in ℕ_{0} (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))$
15	7 14	sylib	$⊢ F \in Poly (S) \to \exists a \in (ℂ^{ℕ_{0}}) \exists n \in ℕ_{0} (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))$
16		reeanv	$⊢ \exists n \in ℕ_{0} \exists m \in ℕ_{0} ((a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \land (b [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} b (k) z^{k}))) \leftrightarrow (\exists n \in ℕ_{0} (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \land \exists m \in ℕ_{0} (b [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} b (k) z^{k})))$
17		simp1l	$⊢ ((F \in Poly (S) \land (a \in (ℂ^{ℕ_{0}}) \land b \in (ℂ^{ℕ_{0}}))) \land (n \in ℕ_{0} \land m \in ℕ_{0}) \land ((a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \land (b [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} b (k) z^{k})))) \to F \in Poly (S)$
18		simp1rl	$⊢ ((F \in Poly (S) \land (a \in (ℂ^{ℕ_{0}}) \land b \in (ℂ^{ℕ_{0}}))) \land (n \in ℕ_{0} \land m \in ℕ_{0}) \land ((a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \land (b [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} b (k) z^{k})))) \to a \in (ℂ^{ℕ_{0}})$
19		simp1rr	$⊢ ((F \in Poly (S) \land (a \in (ℂ^{ℕ_{0}}) \land b \in (ℂ^{ℕ_{0}}))) \land (n \in ℕ_{0} \land m \in ℕ_{0}) \land ((a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \land (b [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} b (k) z^{k})))) \to b \in (ℂ^{ℕ_{0}})$
20		simp2l	$⊢ ((F \in Poly (S) \land (a \in (ℂ^{ℕ_{0}}) \land b \in (ℂ^{ℕ_{0}}))) \land (n \in ℕ_{0} \land m \in ℕ_{0}) \land ((a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \land (b [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} b (k) z^{k})))) \to n \in ℕ_{0}$
21		simp2r	$⊢ ((F \in Poly (S) \land (a \in (ℂ^{ℕ_{0}}) \land b \in (ℂ^{ℕ_{0}}))) \land (n \in ℕ_{0} \land m \in ℕ_{0}) \land ((a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \land (b [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} b (k) z^{k})))) \to m \in ℕ_{0}$
22		simp3ll	$⊢ ((F \in Poly (S) \land (a \in (ℂ^{ℕ_{0}}) \land b \in (ℂ^{ℕ_{0}}))) \land (n \in ℕ_{0} \land m \in ℕ_{0}) \land ((a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \land (b [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} b (k) z^{k})))) \to a [ℤ_{\geq (n + 1)}] = \{0\}$
23		simp3rl	$⊢ ((F \in Poly (S) \land (a \in (ℂ^{ℕ_{0}}) \land b \in (ℂ^{ℕ_{0}}))) \land (n \in ℕ_{0} \land m \in ℕ_{0}) \land ((a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \land (b [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} b (k) z^{k})))) \to b [ℤ_{\geq (m + 1)}] = \{0\}$
24		simp3lr	$⊢ ((F \in Poly (S) \land (a \in (ℂ^{ℕ_{0}}) \land b \in (ℂ^{ℕ_{0}}))) \land (n \in ℕ_{0} \land m \in ℕ_{0}) \land ((a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \land (b [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} b (k) z^{k})))) \to F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})$
25		oveq1	$⊢ z = w \to z^{k} = w^{k}$
26	25	oveq2d	$⊢ z = w \to a (k) z^{k} = a (k) w^{k}$
27	26	sumeq2sdv	$⊢ z = w \to \sum_{k = 0}^{n} a (k) z^{k} = \sum_{k = 0}^{n} a (k) w^{k}$
28		fveq2	$⊢ k = j \to a (k) = a (j)$
29		oveq2	$⊢ k = j \to w^{k} = w^{j}$
30	28 29	oveq12d	$⊢ k = j \to a (k) w^{k} = a (j) w^{j}$
31	30	cbvsumv	$⊢ \sum_{k = 0}^{n} a (k) w^{k} = \sum_{j = 0}^{n} a (j) w^{j}$
32	27 31	eqtrdi	$⊢ z = w \to \sum_{k = 0}^{n} a (k) z^{k} = \sum_{j = 0}^{n} a (j) w^{j}$
33	32	cbvmptv	$⊢ (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}) = (w \in ℂ ⟼ \sum_{j = 0}^{n} a (j) w^{j})$
34	24 33	eqtrdi	$⊢ ((F \in Poly (S) \land (a \in (ℂ^{ℕ_{0}}) \land b \in (ℂ^{ℕ_{0}}))) \land (n \in ℕ_{0} \land m \in ℕ_{0}) \land ((a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \land (b [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} b (k) z^{k})))) \to F = (w \in ℂ ⟼ \sum_{j = 0}^{n} a (j) w^{j})$
35		simp3rr	$⊢ ((F \in Poly (S) \land (a \in (ℂ^{ℕ_{0}}) \land b \in (ℂ^{ℕ_{0}}))) \land (n \in ℕ_{0} \land m \in ℕ_{0}) \land ((a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \land (b [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} b (k) z^{k})))) \to F = (z \in ℂ ⟼ \sum_{k = 0}^{m} b (k) z^{k})$
36	25	oveq2d	$⊢ z = w \to b (k) z^{k} = b (k) w^{k}$
37	36	sumeq2sdv	$⊢ z = w \to \sum_{k = 0}^{m} b (k) z^{k} = \sum_{k = 0}^{m} b (k) w^{k}$
38		fveq2	$⊢ k = j \to b (k) = b (j)$
39	38 29	oveq12d	$⊢ k = j \to b (k) w^{k} = b (j) w^{j}$
40	39	cbvsumv	$⊢ \sum_{k = 0}^{m} b (k) w^{k} = \sum_{j = 0}^{m} b (j) w^{j}$
41	37 40	eqtrdi	$⊢ z = w \to \sum_{k = 0}^{m} b (k) z^{k} = \sum_{j = 0}^{m} b (j) w^{j}$
42	41	cbvmptv	$⊢ (z \in ℂ ⟼ \sum_{k = 0}^{m} b (k) z^{k}) = (w \in ℂ ⟼ \sum_{j = 0}^{m} b (j) w^{j})$
43	35 42	eqtrdi	$⊢ ((F \in Poly (S) \land (a \in (ℂ^{ℕ_{0}}) \land b \in (ℂ^{ℕ_{0}}))) \land (n \in ℕ_{0} \land m \in ℕ_{0}) \land ((a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \land (b [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} b (k) z^{k})))) \to F = (w \in ℂ ⟼ \sum_{j = 0}^{m} b (j) w^{j})$
44	17 18 19 20 21 22 23 34 43	coeeulem	$⊢ ((F \in Poly (S) \land (a \in (ℂ^{ℕ_{0}}) \land b \in (ℂ^{ℕ_{0}}))) \land (n \in ℕ_{0} \land m \in ℕ_{0}) \land ((a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \land (b [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} b (k) z^{k})))) \to a = b$
45	44	3expia	$⊢ ((F \in Poly (S) \land (a \in (ℂ^{ℕ_{0}}) \land b \in (ℂ^{ℕ_{0}}))) \land (n \in ℕ_{0} \land m \in ℕ_{0})) \to (((a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \land (b [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} b (k) z^{k}))) \to a = b)$
46	45	rexlimdvva	$⊢ (F \in Poly (S) \land (a \in (ℂ^{ℕ_{0}}) \land b \in (ℂ^{ℕ_{0}}))) \to (\exists n \in ℕ_{0} \exists m \in ℕ_{0} ((a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \land (b [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} b (k) z^{k}))) \to a = b)$
47	16 46	biimtrrid	$⊢ (F \in Poly (S) \land (a \in (ℂ^{ℕ_{0}}) \land b \in (ℂ^{ℕ_{0}}))) \to ((\exists n \in ℕ_{0} (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \land \exists m \in ℕ_{0} (b [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} b (k) z^{k}))) \to a = b)$
48	47	ralrimivva	$⊢ F \in Poly (S) \to \forall a \in (ℂ^{ℕ_{0}}) \forall b \in (ℂ^{ℕ_{0}}) ((\exists n \in ℕ_{0} (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \land \exists m \in ℕ_{0} (b [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} b (k) z^{k}))) \to a = b)$
49		imaeq1	$⊢ a = b \to a [ℤ_{\geq (n + 1)}] = b [ℤ_{\geq (n + 1)}]$
50	49	eqeq1d	$⊢ a = b \to (a [ℤ_{\geq (n + 1)}] = \{0\} \leftrightarrow b [ℤ_{\geq (n + 1)}] = \{0\})$
51		fveq1	$⊢ a = b \to a (k) = b (k)$
52	51	oveq1d	$⊢ a = b \to a (k) z^{k} = b (k) z^{k}$
53	52	sumeq2sdv	$⊢ a = b \to \sum_{k = 0}^{n} a (k) z^{k} = \sum_{k = 0}^{n} b (k) z^{k}$
54	53	mpteq2dv	$⊢ a = b \to (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k})$
55	54	eqeq2d	$⊢ a = b \to (F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}) \leftrightarrow F = (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k}))$
56	50 55	anbi12d	$⊢ a = b \to ((a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \leftrightarrow (b [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k})))$
57	56	rexbidv	$⊢ a = b \to (\exists n \in ℕ_{0} (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \leftrightarrow \exists n \in ℕ_{0} (b [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k})))$
58		fvoveq1	$⊢ n = m \to ℤ_{\geq (n + 1)} = ℤ_{\geq (m + 1)}$
59	58	imaeq2d	$⊢ n = m \to b [ℤ_{\geq (n + 1)}] = b [ℤ_{\geq (m + 1)}]$
60	59	eqeq1d	$⊢ n = m \to (b [ℤ_{\geq (n + 1)}] = \{0\} \leftrightarrow b [ℤ_{\geq (m + 1)}] = \{0\})$
61		oveq2	$⊢ n = m \to (0 \dots n) = (0 \dots m)$
62	61	sumeq1d	$⊢ n = m \to \sum_{k = 0}^{n} b (k) z^{k} = \sum_{k = 0}^{m} b (k) z^{k}$
63	62	mpteq2dv	$⊢ n = m \to (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k}) = (z \in ℂ ⟼ \sum_{k = 0}^{m} b (k) z^{k})$
64	63	eqeq2d	$⊢ n = m \to (F = (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k}) \leftrightarrow F = (z \in ℂ ⟼ \sum_{k = 0}^{m} b (k) z^{k}))$
65	60 64	anbi12d	$⊢ n = m \to ((b [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k})) \leftrightarrow (b [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} b (k) z^{k})))$
66	65	cbvrexvw	$⊢ \exists n \in ℕ_{0} (b [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k})) \leftrightarrow \exists m \in ℕ_{0} (b [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} b (k) z^{k}))$
67	57 66	bitrdi	$⊢ a = b \to (\exists n \in ℕ_{0} (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \leftrightarrow \exists m \in ℕ_{0} (b [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} b (k) z^{k})))$
68	67	reu4	$⊢ \exists! a \in (ℂ^{ℕ_{0}}) \exists n \in ℕ_{0} (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \leftrightarrow (\exists a \in (ℂ^{ℕ_{0}}) \exists n \in ℕ_{0} (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \land \forall a \in (ℂ^{ℕ_{0}}) \forall b \in (ℂ^{ℕ_{0}}) ((\exists n \in ℕ_{0} (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k})) \land \exists m \in ℕ_{0} (b [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} b (k) z^{k}))) \to a = b))$
69	15 48 68	sylanbrc	$⊢ F \in Poly (S) \to \exists! a \in (ℂ^{ℕ_{0}}) \exists n \in ℕ_{0} (a [ℤ_{\geq (n + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{n} a (k) z^{k}))$

Metamath Proof Explorer

Theorem coeeu

Proof