plyadd

Description: The sum of two polynomials is a polynomial. (Contributed by Mario Carneiro, 21-Jul-2014)

	Ref	Expression
Hypotheses	plyadd.1	$⊢ φ \to F \in Poly (S)$
	plyadd.2	$⊢ φ \to G \in Poly (S)$
	plyadd.3	$⊢ (φ \land (x \in S \land y \in S)) \to x + y \in S$
Assertion	plyadd	$⊢ φ \to F +_{f} G \in Poly (S)$

Proof

Step	Hyp	Ref	Expression
1		plyadd.1	$⊢ φ \to F \in Poly (S)$
2		plyadd.2	$⊢ φ \to G \in Poly (S)$
3		plyadd.3	$⊢ (φ \land (x \in S \land y \in S)) \to x + y \in S$
4		elply2	$⊢ F \in Poly (S) \leftrightarrow (S \subseteq ℂ \land \exists m \in ℕ_{0} \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) (a [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} a (k) z^{k})))$
5	4	simprbi	$⊢ F \in Poly (S) \to \exists m \in ℕ_{0} \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) (a [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} a (k) z^{k}))$
6	1 5	syl	$⊢ φ \to \exists m \in ℕ_{0} \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) (a [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} a (k) z^{k}))$
7		elply2	$⊢ G \in Poly (S) \leftrightarrow (S \subseteq ℂ \land \exists n \in ℕ_{0} \exists b \in ({(S \cup \{0\})}^{ℕ_{0}}) (b [ℤ_{\geq (n + 1)}] = \{0\} \land G = (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k})))$
8	7	simprbi	$⊢ G \in Poly (S) \to \exists n \in ℕ_{0} \exists b \in ({(S \cup \{0\})}^{ℕ_{0}}) (b [ℤ_{\geq (n + 1)}] = \{0\} \land G = (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k}))$
9	2 8	syl	$⊢ φ \to \exists n \in ℕ_{0} \exists b \in ({(S \cup \{0\})}^{ℕ_{0}}) (b [ℤ_{\geq (n + 1)}] = \{0\} \land G = (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k}))$
10		reeanv	$⊢ \exists m \in ℕ_{0} \exists n \in ℕ_{0} (\exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) (a [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} a (k) z^{k})) \land \exists b \in ({(S \cup \{0\})}^{ℕ_{0}}) (b [ℤ_{\geq (n + 1)}] = \{0\} \land G = (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k}))) \leftrightarrow (\exists m \in ℕ_{0} \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) (a [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} a (k) z^{k})) \land \exists n \in ℕ_{0} \exists b \in ({(S \cup \{0\})}^{ℕ_{0}}) (b [ℤ_{\geq (n + 1)}] = \{0\} \land G = (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k})))$
11		reeanv	$⊢ \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) \exists b \in ({(S \cup \{0\})}^{ℕ_{0}}) ((a [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} a (k) z^{k})) \land (b [ℤ_{\geq (n + 1)}] = \{0\} \land G = (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k}))) \leftrightarrow (\exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) (a [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} a (k) z^{k})) \land \exists b \in ({(S \cup \{0\})}^{ℕ_{0}}) (b [ℤ_{\geq (n + 1)}] = \{0\} \land G = (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k})))$
12		simp1l	$⊢ ((φ \land (m \in ℕ_{0} \land n \in ℕ_{0})) \land (a \in ({(S \cup \{0\})}^{ℕ_{0}}) \land b \in ({(S \cup \{0\})}^{ℕ_{0}})) \land ((a [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} a (k) z^{k})) \land (b [ℤ_{\geq (n + 1)}] = \{0\} \land G = (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k})))) \to φ$
13	12 1	syl	$⊢ ((φ \land (m \in ℕ_{0} \land n \in ℕ_{0})) \land (a \in ({(S \cup \{0\})}^{ℕ_{0}}) \land b \in ({(S \cup \{0\})}^{ℕ_{0}})) \land ((a [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} a (k) z^{k})) \land (b [ℤ_{\geq (n + 1)}] = \{0\} \land G = (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k})))) \to F \in Poly (S)$
14	12 2	syl	$⊢ ((φ \land (m \in ℕ_{0} \land n \in ℕ_{0})) \land (a \in ({(S \cup \{0\})}^{ℕ_{0}}) \land b \in ({(S \cup \{0\})}^{ℕ_{0}})) \land ((a [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} a (k) z^{k})) \land (b [ℤ_{\geq (n + 1)}] = \{0\} \land G = (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k})))) \to G \in Poly (S)$
15	12 3	sylan	$⊢ (((φ \land (m \in ℕ_{0} \land n \in ℕ_{0})) \land (a \in ({(S \cup \{0\})}^{ℕ_{0}}) \land b \in ({(S \cup \{0\})}^{ℕ_{0}})) \land ((a [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} a (k) z^{k})) \land (b [ℤ_{\geq (n + 1)}] = \{0\} \land G = (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k})))) \land (x \in S \land y \in S)) \to x + y \in S$
16		simp1rl	$⊢ ((φ \land (m \in ℕ_{0} \land n \in ℕ_{0})) \land (a \in ({(S \cup \{0\})}^{ℕ_{0}}) \land b \in ({(S \cup \{0\})}^{ℕ_{0}})) \land ((a [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} a (k) z^{k})) \land (b [ℤ_{\geq (n + 1)}] = \{0\} \land G = (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k})))) \to m \in ℕ_{0}$
17		simp1rr	$⊢ ((φ \land (m \in ℕ_{0} \land n \in ℕ_{0})) \land (a \in ({(S \cup \{0\})}^{ℕ_{0}}) \land b \in ({(S \cup \{0\})}^{ℕ_{0}})) \land ((a [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} a (k) z^{k})) \land (b [ℤ_{\geq (n + 1)}] = \{0\} \land G = (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k})))) \to n \in ℕ_{0}$
18		simp2l	$⊢ ((φ \land (m \in ℕ_{0} \land n \in ℕ_{0})) \land (a \in ({(S \cup \{0\})}^{ℕ_{0}}) \land b \in ({(S \cup \{0\})}^{ℕ_{0}})) \land ((a [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} a (k) z^{k})) \land (b [ℤ_{\geq (n + 1)}] = \{0\} \land G = (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k})))) \to a \in ({(S \cup \{0\})}^{ℕ_{0}})$
19		simp2r	$⊢ ((φ \land (m \in ℕ_{0} \land n \in ℕ_{0})) \land (a \in ({(S \cup \{0\})}^{ℕ_{0}}) \land b \in ({(S \cup \{0\})}^{ℕ_{0}})) \land ((a [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} a (k) z^{k})) \land (b [ℤ_{\geq (n + 1)}] = \{0\} \land G = (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k})))) \to b \in ({(S \cup \{0\})}^{ℕ_{0}})$
20		simp3ll	$⊢ ((φ \land (m \in ℕ_{0} \land n \in ℕ_{0})) \land (a \in ({(S \cup \{0\})}^{ℕ_{0}}) \land b \in ({(S \cup \{0\})}^{ℕ_{0}})) \land ((a [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} a (k) z^{k})) \land (b [ℤ_{\geq (n + 1)}] = \{0\} \land G = (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k})))) \to a [ℤ_{\geq (m + 1)}] = \{0\}$
21		simp3rl	$⊢ ((φ \land (m \in ℕ_{0} \land n \in ℕ_{0})) \land (a \in ({(S \cup \{0\})}^{ℕ_{0}}) \land b \in ({(S \cup \{0\})}^{ℕ_{0}})) \land ((a [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} a (k) z^{k})) \land (b [ℤ_{\geq (n + 1)}] = \{0\} \land G = (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k})))) \to b [ℤ_{\geq (n + 1)}] = \{0\}$
22		simp3lr	$⊢ ((φ \land (m \in ℕ_{0} \land n \in ℕ_{0})) \land (a \in ({(S \cup \{0\})}^{ℕ_{0}}) \land b \in ({(S \cup \{0\})}^{ℕ_{0}})) \land ((a [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} a (k) z^{k})) \land (b [ℤ_{\geq (n + 1)}] = \{0\} \land G = (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k})))) \to F = (z \in ℂ ⟼ \sum_{k = 0}^{m} a (k) z^{k})$
23		oveq1	$⊢ z = w \to z^{k} = w^{k}$
24	23	oveq2d	$⊢ z = w \to a (k) z^{k} = a (k) w^{k}$
25	24	sumeq2sdv	$⊢ z = w \to \sum_{k = 0}^{m} a (k) z^{k} = \sum_{k = 0}^{m} a (k) w^{k}$
26		fveq2	$⊢ k = j \to a (k) = a (j)$
27		oveq2	$⊢ k = j \to w^{k} = w^{j}$
28	26 27	oveq12d	$⊢ k = j \to a (k) w^{k} = a (j) w^{j}$
29	28	cbvsumv	$⊢ \sum_{k = 0}^{m} a (k) w^{k} = \sum_{j = 0}^{m} a (j) w^{j}$
30	25 29	eqtrdi	$⊢ z = w \to \sum_{k = 0}^{m} a (k) z^{k} = \sum_{j = 0}^{m} a (j) w^{j}$
31	30	cbvmptv	$⊢ (z \in ℂ ⟼ \sum_{k = 0}^{m} a (k) z^{k}) = (w \in ℂ ⟼ \sum_{j = 0}^{m} a (j) w^{j})$
32	22 31	eqtrdi	$⊢ ((φ \land (m \in ℕ_{0} \land n \in ℕ_{0})) \land (a \in ({(S \cup \{0\})}^{ℕ_{0}}) \land b \in ({(S \cup \{0\})}^{ℕ_{0}})) \land ((a [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} a (k) z^{k})) \land (b [ℤ_{\geq (n + 1)}] = \{0\} \land G = (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k})))) \to F = (w \in ℂ ⟼ \sum_{j = 0}^{m} a (j) w^{j})$
33		simp3rr	$⊢ ((φ \land (m \in ℕ_{0} \land n \in ℕ_{0})) \land (a \in ({(S \cup \{0\})}^{ℕ_{0}}) \land b \in ({(S \cup \{0\})}^{ℕ_{0}})) \land ((a [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} a (k) z^{k})) \land (b [ℤ_{\geq (n + 1)}] = \{0\} \land G = (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k})))) \to G = (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k})$
34	23	oveq2d	$⊢ z = w \to b (k) z^{k} = b (k) w^{k}$
35	34	sumeq2sdv	$⊢ z = w \to \sum_{k = 0}^{n} b (k) z^{k} = \sum_{k = 0}^{n} b (k) w^{k}$
36		fveq2	$⊢ k = j \to b (k) = b (j)$
37	36 27	oveq12d	$⊢ k = j \to b (k) w^{k} = b (j) w^{j}$
38	37	cbvsumv	$⊢ \sum_{k = 0}^{n} b (k) w^{k} = \sum_{j = 0}^{n} b (j) w^{j}$
39	35 38	eqtrdi	$⊢ z = w \to \sum_{k = 0}^{n} b (k) z^{k} = \sum_{j = 0}^{n} b (j) w^{j}$
40	39	cbvmptv	$⊢ (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k}) = (w \in ℂ ⟼ \sum_{j = 0}^{n} b (j) w^{j})$
41	33 40	eqtrdi	$⊢ ((φ \land (m \in ℕ_{0} \land n \in ℕ_{0})) \land (a \in ({(S \cup \{0\})}^{ℕ_{0}}) \land b \in ({(S \cup \{0\})}^{ℕ_{0}})) \land ((a [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} a (k) z^{k})) \land (b [ℤ_{\geq (n + 1)}] = \{0\} \land G = (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k})))) \to G = (w \in ℂ ⟼ \sum_{j = 0}^{n} b (j) w^{j})$
42	13 14 15 16 17 18 19 20 21 32 41	plyaddlem	$⊢ ((φ \land (m \in ℕ_{0} \land n \in ℕ_{0})) \land (a \in ({(S \cup \{0\})}^{ℕ_{0}}) \land b \in ({(S \cup \{0\})}^{ℕ_{0}})) \land ((a [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} a (k) z^{k})) \land (b [ℤ_{\geq (n + 1)}] = \{0\} \land G = (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k})))) \to F +_{f} G \in Poly (S)$
43	42	3expia	$⊢ ((φ \land (m \in ℕ_{0} \land n \in ℕ_{0})) \land (a \in ({(S \cup \{0\})}^{ℕ_{0}}) \land b \in ({(S \cup \{0\})}^{ℕ_{0}}))) \to (((a [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} a (k) z^{k})) \land (b [ℤ_{\geq (n + 1)}] = \{0\} \land G = (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k}))) \to F +_{f} G \in Poly (S))$
44	43	rexlimdvva	$⊢ (φ \land (m \in ℕ_{0} \land n \in ℕ_{0})) \to (\exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) \exists b \in ({(S \cup \{0\})}^{ℕ_{0}}) ((a [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} a (k) z^{k})) \land (b [ℤ_{\geq (n + 1)}] = \{0\} \land G = (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k}))) \to F +_{f} G \in Poly (S))$
45	11 44	biimtrrid	$⊢ (φ \land (m \in ℕ_{0} \land n \in ℕ_{0})) \to ((\exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) (a [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} a (k) z^{k})) \land \exists b \in ({(S \cup \{0\})}^{ℕ_{0}}) (b [ℤ_{\geq (n + 1)}] = \{0\} \land G = (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k}))) \to F +_{f} G \in Poly (S))$
46	45	rexlimdvva	$⊢ φ \to (\exists m \in ℕ_{0} \exists n \in ℕ_{0} (\exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) (a [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} a (k) z^{k})) \land \exists b \in ({(S \cup \{0\})}^{ℕ_{0}}) (b [ℤ_{\geq (n + 1)}] = \{0\} \land G = (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k}))) \to F +_{f} G \in Poly (S))$
47	10 46	biimtrrid	$⊢ φ \to ((\exists m \in ℕ_{0} \exists a \in ({(S \cup \{0\})}^{ℕ_{0}}) (a [ℤ_{\geq (m + 1)}] = \{0\} \land F = (z \in ℂ ⟼ \sum_{k = 0}^{m} a (k) z^{k})) \land \exists n \in ℕ_{0} \exists b \in ({(S \cup \{0\})}^{ℕ_{0}}) (b [ℤ_{\geq (n + 1)}] = \{0\} \land G = (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k}))) \to F +_{f} G \in Poly (S))$
48	6 9 47	mp2and	$⊢ φ \to F +_{f} G \in Poly (S)$

Metamath Proof Explorer

Theorem plyadd

Proof