plymul

Description: The product 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$
	plymul.4	$⊢ (φ \land (x \in S \land y \in S)) \to x y \in S$
Assertion	plymul	$⊢ φ \to F \times_{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		plymul.4	$⊢ (φ \land (x \in S \land y \in S)) \to x y \in S$
5		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})))$
6	5	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}))$
7	1 6	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}))$
8		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})))$
9	8	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}))$
10	2 9	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}))$
11		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})))$
12		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})))$
13		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 φ$
14	13 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)$
15	13 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)$
16	13 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$
17		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}$
18		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}$
19		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}})$
20		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}})$
21		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\}$
22		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\}$
23		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})$
24		oveq1	$⊢ z = w \to z^{k} = w^{k}$
25	24	oveq2d	$⊢ z = w \to a (k) z^{k} = a (k) w^{k}$
26	25	sumeq2sdv	$⊢ z = w \to \sum_{k = 0}^{m} a (k) z^{k} = \sum_{k = 0}^{m} a (k) w^{k}$
27		fveq2	$⊢ k = j \to a (k) = a (j)$
28		oveq2	$⊢ k = j \to w^{k} = w^{j}$
29	27 28	oveq12d	$⊢ k = j \to a (k) w^{k} = a (j) w^{j}$
30	29	cbvsumv	$⊢ \sum_{k = 0}^{m} a (k) w^{k} = \sum_{j = 0}^{m} a (j) w^{j}$
31	26 30	eqtrdi	$⊢ z = w \to \sum_{k = 0}^{m} a (k) z^{k} = \sum_{j = 0}^{m} a (j) w^{j}$
32	31	cbvmptv	$⊢ (z \in ℂ ⟼ \sum_{k = 0}^{m} a (k) z^{k}) = (w \in ℂ ⟼ \sum_{j = 0}^{m} a (j) w^{j})$
33	23 32	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})$
34		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})$
35	24	oveq2d	$⊢ z = w \to b (k) z^{k} = b (k) w^{k}$
36	35	sumeq2sdv	$⊢ z = w \to \sum_{k = 0}^{n} b (k) z^{k} = \sum_{k = 0}^{n} b (k) w^{k}$
37		fveq2	$⊢ k = j \to b (k) = b (j)$
38	37 28	oveq12d	$⊢ k = j \to b (k) w^{k} = b (j) w^{j}$
39	38	cbvsumv	$⊢ \sum_{k = 0}^{n} b (k) w^{k} = \sum_{j = 0}^{n} b (j) w^{j}$
40	36 39	eqtrdi	$⊢ z = w \to \sum_{k = 0}^{n} b (k) z^{k} = \sum_{j = 0}^{n} b (j) w^{j}$
41	40	cbvmptv	$⊢ (z \in ℂ ⟼ \sum_{k = 0}^{n} b (k) z^{k}) = (w \in ℂ ⟼ \sum_{j = 0}^{n} b (j) w^{j})$
42	34 41	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})$
43	13 4	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$
44	14 15 16 17 18 19 20 21 22 33 42 43	plymullem	$⊢ ((φ \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 \times_{f} G \in Poly (S)$
45	44	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 \times_{f} G \in Poly (S))$
46	45	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 \times_{f} G \in Poly (S))$
47	12 46	syl5bir	$⊢ (φ \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 \times_{f} G \in Poly (S))$
48	47	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 \times_{f} G \in Poly (S))$
49	11 48	syl5bir	$⊢ φ \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 \times_{f} G \in Poly (S))$
50	7 10 49	mp2and	$⊢ φ \to F \times_{f} G \in Poly (S)$

Metamath Proof Explorer

Theorem plymul

Proof