# Metamath Proof Explorer

## Theorem plymullem

Description: Lemma for plymul . (Contributed by Mario Carneiro, 21-Jul-2014)

Ref Expression
Hypotheses plyadd.1 ${⊢}{\phi }\to {F}\in \mathrm{Poly}\left({S}\right)$
plyadd.2 ${⊢}{\phi }\to {G}\in \mathrm{Poly}\left({S}\right)$
plyadd.3 ${⊢}\left({\phi }\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to {x}+{y}\in {S}$
plyadd.m ${⊢}{\phi }\to {M}\in {ℕ}_{0}$
plyadd.n ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
plyadd.a ${⊢}{\phi }\to {A}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)$
plyadd.b ${⊢}{\phi }\to {B}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)$
plyadd.a2 ${⊢}{\phi }\to {A}\left[{ℤ}_{\ge \left({M}+1\right)}\right]=\left\{0\right\}$
plyadd.b2 ${⊢}{\phi }\to {B}\left[{ℤ}_{\ge \left({N}+1\right)}\right]=\left\{0\right\}$
plyadd.f ${⊢}{\phi }\to {F}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{M}}{A}\left({k}\right){{z}}^{{k}}\right)$
plyadd.g ${⊢}{\phi }\to {G}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{N}}{B}\left({k}\right){{z}}^{{k}}\right)$
plymul.x ${⊢}\left({\phi }\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to {x}{y}\in {S}$
Assertion plymullem ${⊢}{\phi }\to {F}{×}_{f}{G}\in \mathrm{Poly}\left({S}\right)$

### Proof

Step Hyp Ref Expression
1 plyadd.1 ${⊢}{\phi }\to {F}\in \mathrm{Poly}\left({S}\right)$
2 plyadd.2 ${⊢}{\phi }\to {G}\in \mathrm{Poly}\left({S}\right)$
3 plyadd.3 ${⊢}\left({\phi }\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to {x}+{y}\in {S}$
4 plyadd.m ${⊢}{\phi }\to {M}\in {ℕ}_{0}$
5 plyadd.n ${⊢}{\phi }\to {N}\in {ℕ}_{0}$
6 plyadd.a ${⊢}{\phi }\to {A}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)$
7 plyadd.b ${⊢}{\phi }\to {B}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)$
8 plyadd.a2 ${⊢}{\phi }\to {A}\left[{ℤ}_{\ge \left({M}+1\right)}\right]=\left\{0\right\}$
9 plyadd.b2 ${⊢}{\phi }\to {B}\left[{ℤ}_{\ge \left({N}+1\right)}\right]=\left\{0\right\}$
10 plyadd.f ${⊢}{\phi }\to {F}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{M}}{A}\left({k}\right){{z}}^{{k}}\right)$
11 plyadd.g ${⊢}{\phi }\to {G}=\left({z}\in ℂ⟼\sum _{{k}=0}^{{N}}{B}\left({k}\right){{z}}^{{k}}\right)$
12 plymul.x ${⊢}\left({\phi }\wedge \left({x}\in {S}\wedge {y}\in {S}\right)\right)\to {x}{y}\in {S}$
13 plybss ${⊢}{F}\in \mathrm{Poly}\left({S}\right)\to {S}\subseteq ℂ$
14 1 13 syl ${⊢}{\phi }\to {S}\subseteq ℂ$
15 0cnd ${⊢}{\phi }\to 0\in ℂ$
16 15 snssd ${⊢}{\phi }\to \left\{0\right\}\subseteq ℂ$
17 14 16 unssd ${⊢}{\phi }\to {S}\cup \left\{0\right\}\subseteq ℂ$
18 cnex ${⊢}ℂ\in \mathrm{V}$
19 ssexg ${⊢}\left({S}\cup \left\{0\right\}\subseteq ℂ\wedge ℂ\in \mathrm{V}\right)\to {S}\cup \left\{0\right\}\in \mathrm{V}$
20 17 18 19 sylancl ${⊢}{\phi }\to {S}\cup \left\{0\right\}\in \mathrm{V}$
21 nn0ex ${⊢}{ℕ}_{0}\in \mathrm{V}$
22 elmapg ${⊢}\left({S}\cup \left\{0\right\}\in \mathrm{V}\wedge {ℕ}_{0}\in \mathrm{V}\right)\to \left({A}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)↔{A}:{ℕ}_{0}⟶{S}\cup \left\{0\right\}\right)$
23 20 21 22 sylancl ${⊢}{\phi }\to \left({A}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)↔{A}:{ℕ}_{0}⟶{S}\cup \left\{0\right\}\right)$
24 6 23 mpbid ${⊢}{\phi }\to {A}:{ℕ}_{0}⟶{S}\cup \left\{0\right\}$
25 24 17 fssd ${⊢}{\phi }\to {A}:{ℕ}_{0}⟶ℂ$
26 elmapg ${⊢}\left({S}\cup \left\{0\right\}\in \mathrm{V}\wedge {ℕ}_{0}\in \mathrm{V}\right)\to \left({B}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)↔{B}:{ℕ}_{0}⟶{S}\cup \left\{0\right\}\right)$
27 20 21 26 sylancl ${⊢}{\phi }\to \left({B}\in \left({\left({S}\cup \left\{0\right\}\right)}^{{ℕ}_{0}}\right)↔{B}:{ℕ}_{0}⟶{S}\cup \left\{0\right\}\right)$
28 7 27 mpbid ${⊢}{\phi }\to {B}:{ℕ}_{0}⟶{S}\cup \left\{0\right\}$
29 28 17 fssd ${⊢}{\phi }\to {B}:{ℕ}_{0}⟶ℂ$
30 1 2 4 5 25 29 8 9 10 11 plymullem1 ${⊢}{\phi }\to {F}{×}_{f}{G}=\left({z}\in ℂ⟼\sum _{{n}=0}^{{M}+{N}}\sum _{{k}=0}^{{n}}{A}\left({k}\right){B}\left({n}-{k}\right){{z}}^{{n}}\right)$
31 4 5 nn0addcld ${⊢}{\phi }\to {M}+{N}\in {ℕ}_{0}$
32 eqid ${⊢}{S}\cup \left\{0\right\}={S}\cup \left\{0\right\}$
33 14 32 3 un0addcl ${⊢}\left({\phi }\wedge \left({x}\in \left({S}\cup \left\{0\right\}\right)\wedge {y}\in \left({S}\cup \left\{0\right\}\right)\right)\right)\to {x}+{y}\in \left({S}\cup \left\{0\right\}\right)$
34 fzfid ${⊢}{\phi }\to \left(0\dots {n}\right)\in \mathrm{Fin}$
35 elfznn0 ${⊢}{k}\in \left(0\dots {n}\right)\to {k}\in {ℕ}_{0}$
36 ffvelrn ${⊢}\left({A}:{ℕ}_{0}⟶{S}\cup \left\{0\right\}\wedge {k}\in {ℕ}_{0}\right)\to {A}\left({k}\right)\in \left({S}\cup \left\{0\right\}\right)$
37 24 35 36 syl2an ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {n}\right)\right)\to {A}\left({k}\right)\in \left({S}\cup \left\{0\right\}\right)$
38 fznn0sub ${⊢}{k}\in \left(0\dots {n}\right)\to {n}-{k}\in {ℕ}_{0}$
39 ffvelrn ${⊢}\left({B}:{ℕ}_{0}⟶{S}\cup \left\{0\right\}\wedge {n}-{k}\in {ℕ}_{0}\right)\to {B}\left({n}-{k}\right)\in \left({S}\cup \left\{0\right\}\right)$
40 28 38 39 syl2an ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {n}\right)\right)\to {B}\left({n}-{k}\right)\in \left({S}\cup \left\{0\right\}\right)$
41 37 40 jca ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {n}\right)\right)\to \left({A}\left({k}\right)\in \left({S}\cup \left\{0\right\}\right)\wedge {B}\left({n}-{k}\right)\in \left({S}\cup \left\{0\right\}\right)\right)$
42 14 32 12 un0mulcl ${⊢}\left({\phi }\wedge \left({x}\in \left({S}\cup \left\{0\right\}\right)\wedge {y}\in \left({S}\cup \left\{0\right\}\right)\right)\right)\to {x}{y}\in \left({S}\cup \left\{0\right\}\right)$
43 42 caovclg ${⊢}\left({\phi }\wedge \left({A}\left({k}\right)\in \left({S}\cup \left\{0\right\}\right)\wedge {B}\left({n}-{k}\right)\in \left({S}\cup \left\{0\right\}\right)\right)\right)\to {A}\left({k}\right){B}\left({n}-{k}\right)\in \left({S}\cup \left\{0\right\}\right)$
44 41 43 syldan ${⊢}\left({\phi }\wedge {k}\in \left(0\dots {n}\right)\right)\to {A}\left({k}\right){B}\left({n}-{k}\right)\in \left({S}\cup \left\{0\right\}\right)$
45 ssun2 ${⊢}\left\{0\right\}\subseteq {S}\cup \left\{0\right\}$
46 c0ex ${⊢}0\in \mathrm{V}$
47 46 snss ${⊢}0\in \left({S}\cup \left\{0\right\}\right)↔\left\{0\right\}\subseteq {S}\cup \left\{0\right\}$
48 45 47 mpbir ${⊢}0\in \left({S}\cup \left\{0\right\}\right)$
49 48 a1i ${⊢}{\phi }\to 0\in \left({S}\cup \left\{0\right\}\right)$
50 17 33 34 44 49 fsumcllem ${⊢}{\phi }\to \sum _{{k}=0}^{{n}}{A}\left({k}\right){B}\left({n}-{k}\right)\in \left({S}\cup \left\{0\right\}\right)$
51 50 adantr ${⊢}\left({\phi }\wedge {n}\in \left(0\dots {M}+{N}\right)\right)\to \sum _{{k}=0}^{{n}}{A}\left({k}\right){B}\left({n}-{k}\right)\in \left({S}\cup \left\{0\right\}\right)$
52 17 31 51 elplyd ${⊢}{\phi }\to \left({z}\in ℂ⟼\sum _{{n}=0}^{{M}+{N}}\sum _{{k}=0}^{{n}}{A}\left({k}\right){B}\left({n}-{k}\right){{z}}^{{n}}\right)\in \mathrm{Poly}\left({S}\cup \left\{0\right\}\right)$
53 30 52 eqeltrd ${⊢}{\phi }\to {F}{×}_{f}{G}\in \mathrm{Poly}\left({S}\cup \left\{0\right\}\right)$
54 plyun0 ${⊢}\mathrm{Poly}\left({S}\cup \left\{0\right\}\right)=\mathrm{Poly}\left({S}\right)$
55 53 54 eleqtrdi ${⊢}{\phi }\to {F}{×}_{f}{G}\in \mathrm{Poly}\left({S}\right)$