# Metamath Proof Explorer

## Theorem cply1mul

Description: The product of two constant polynomials is a constant polynomial. (Contributed by AV, 18-Nov-2019)

Ref Expression
Hypotheses cply1mul.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
cply1mul.b ${⊢}{B}={\mathrm{Base}}_{{P}}$
cply1mul.0
cply1mul.m
Assertion cply1mul

### Proof

Step Hyp Ref Expression
1 cply1mul.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
2 cply1mul.b ${⊢}{B}={\mathrm{Base}}_{{P}}$
3 cply1mul.0
4 cply1mul.m
5 eqid ${⊢}{\cdot }_{{R}}={\cdot }_{{R}}$
6 1 4 5 2 coe1mul
7 6 3expb
10 oveq2 ${⊢}{s}={n}\to \left(0\dots {s}\right)=\left(0\dots {n}\right)$
11 fvoveq1 ${⊢}{s}={n}\to {\mathrm{coe}}_{1}\left({G}\right)\left({s}-{k}\right)={\mathrm{coe}}_{1}\left({G}\right)\left({n}-{k}\right)$
12 11 oveq2d ${⊢}{s}={n}\to {\mathrm{coe}}_{1}\left({F}\right)\left({k}\right){\cdot }_{{R}}{\mathrm{coe}}_{1}\left({G}\right)\left({s}-{k}\right)={\mathrm{coe}}_{1}\left({F}\right)\left({k}\right){\cdot }_{{R}}{\mathrm{coe}}_{1}\left({G}\right)\left({n}-{k}\right)$
13 10 12 mpteq12dv ${⊢}{s}={n}\to \left({k}\in \left(0\dots {s}\right)⟼{\mathrm{coe}}_{1}\left({F}\right)\left({k}\right){\cdot }_{{R}}{\mathrm{coe}}_{1}\left({G}\right)\left({s}-{k}\right)\right)=\left({k}\in \left(0\dots {n}\right)⟼{\mathrm{coe}}_{1}\left({F}\right)\left({k}\right){\cdot }_{{R}}{\mathrm{coe}}_{1}\left({G}\right)\left({n}-{k}\right)\right)$
14 13 oveq2d ${⊢}{s}={n}\to \underset{{k}=0}{\overset{{s}}{{\sum }_{{R}}}}\left({\mathrm{coe}}_{1}\left({F}\right)\left({k}\right){\cdot }_{{R}}{\mathrm{coe}}_{1}\left({G}\right)\left({s}-{k}\right)\right)=\underset{{k}=0}{\overset{{n}}{{\sum }_{{R}}}}\left({\mathrm{coe}}_{1}\left({F}\right)\left({k}\right){\cdot }_{{R}}{\mathrm{coe}}_{1}\left({G}\right)\left({n}-{k}\right)\right)$
16 nnnn0 ${⊢}{n}\in ℕ\to {n}\in {ℕ}_{0}$
18 ovexd
19 9 15 17 18 fvmptd
20 r19.26
21 oveq2 ${⊢}{k}=0\to {n}-{k}={n}-0$
22 nncn ${⊢}{n}\in ℕ\to {n}\in ℂ$
23 22 subid1d ${⊢}{n}\in ℕ\to {n}-0={n}$
24 23 adantr ${⊢}\left({n}\in ℕ\wedge {k}\in \left(0\dots {n}\right)\right)\to {n}-0={n}$
25 21 24 sylan9eqr ${⊢}\left(\left({n}\in ℕ\wedge {k}\in \left(0\dots {n}\right)\right)\wedge {k}=0\right)\to {n}-{k}={n}$
26 simpll ${⊢}\left(\left({n}\in ℕ\wedge {k}\in \left(0\dots {n}\right)\right)\wedge {k}=0\right)\to {n}\in ℕ$
27 25 26 eqeltrd ${⊢}\left(\left({n}\in ℕ\wedge {k}\in \left(0\dots {n}\right)\right)\wedge {k}=0\right)\to {n}-{k}\in ℕ$
28 fveqeq2
29 28 rspcv
30 27 29 syl
31 oveq2
32 simpll ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({F}\in {B}\wedge {G}\in {B}\right)\right)\wedge \left(\left({n}\in ℕ\wedge {k}\in \left(0\dots {n}\right)\right)\wedge {k}=0\right)\right)\to {R}\in \mathrm{Ring}$
33 simprl ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({F}\in {B}\wedge {G}\in {B}\right)\right)\to {F}\in {B}$
34 elfznn0 ${⊢}{k}\in \left(0\dots {n}\right)\to {k}\in {ℕ}_{0}$
35 34 adantl ${⊢}\left({n}\in ℕ\wedge {k}\in \left(0\dots {n}\right)\right)\to {k}\in {ℕ}_{0}$
36 35 adantr ${⊢}\left(\left({n}\in ℕ\wedge {k}\in \left(0\dots {n}\right)\right)\wedge {k}=0\right)\to {k}\in {ℕ}_{0}$
37 eqid ${⊢}{\mathrm{coe}}_{1}\left({F}\right)={\mathrm{coe}}_{1}\left({F}\right)$
38 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
39 37 2 1 38 coe1fvalcl ${⊢}\left({F}\in {B}\wedge {k}\in {ℕ}_{0}\right)\to {\mathrm{coe}}_{1}\left({F}\right)\left({k}\right)\in {\mathrm{Base}}_{{R}}$
40 33 36 39 syl2an ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({F}\in {B}\wedge {G}\in {B}\right)\right)\wedge \left(\left({n}\in ℕ\wedge {k}\in \left(0\dots {n}\right)\right)\wedge {k}=0\right)\right)\to {\mathrm{coe}}_{1}\left({F}\right)\left({k}\right)\in {\mathrm{Base}}_{{R}}$
41 38 5 3 ringrz
42 32 40 41 syl2anc
43 31 42 sylan9eqr
44 43 ex
45 44 expcom
46 45 com23
47 30 46 syldc
48 47 expd
49 48 com24
51 50 com13
52 neqne ${⊢}¬{k}=0\to {k}\ne 0$
53 52 34 anim12ci ${⊢}\left(¬{k}=0\wedge {k}\in \left(0\dots {n}\right)\right)\to \left({k}\in {ℕ}_{0}\wedge {k}\ne 0\right)$
54 elnnne0 ${⊢}{k}\in ℕ↔\left({k}\in {ℕ}_{0}\wedge {k}\ne 0\right)$
55 53 54 sylibr ${⊢}\left(¬{k}=0\wedge {k}\in \left(0\dots {n}\right)\right)\to {k}\in ℕ$
56 fveqeq2
57 56 rspcv
58 55 57 syl
59 oveq1
60 simpll ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({F}\in {B}\wedge {G}\in {B}\right)\right)\wedge {k}\in \left(0\dots {n}\right)\right)\to {R}\in \mathrm{Ring}$
61 2 eleq2i ${⊢}{G}\in {B}↔{G}\in {\mathrm{Base}}_{{P}}$
62 61 biimpi ${⊢}{G}\in {B}\to {G}\in {\mathrm{Base}}_{{P}}$
63 62 adantl ${⊢}\left({F}\in {B}\wedge {G}\in {B}\right)\to {G}\in {\mathrm{Base}}_{{P}}$
64 63 adantl ${⊢}\left({R}\in \mathrm{Ring}\wedge \left({F}\in {B}\wedge {G}\in {B}\right)\right)\to {G}\in {\mathrm{Base}}_{{P}}$
65 fznn0sub ${⊢}{k}\in \left(0\dots {n}\right)\to {n}-{k}\in {ℕ}_{0}$
66 eqid ${⊢}{\mathrm{coe}}_{1}\left({G}\right)={\mathrm{coe}}_{1}\left({G}\right)$
67 eqid ${⊢}{\mathrm{Base}}_{{P}}={\mathrm{Base}}_{{P}}$
68 66 67 1 38 coe1fvalcl ${⊢}\left({G}\in {\mathrm{Base}}_{{P}}\wedge {n}-{k}\in {ℕ}_{0}\right)\to {\mathrm{coe}}_{1}\left({G}\right)\left({n}-{k}\right)\in {\mathrm{Base}}_{{R}}$
69 64 65 68 syl2an ${⊢}\left(\left({R}\in \mathrm{Ring}\wedge \left({F}\in {B}\wedge {G}\in {B}\right)\right)\wedge {k}\in \left(0\dots {n}\right)\right)\to {\mathrm{coe}}_{1}\left({G}\right)\left({n}-{k}\right)\in {\mathrm{Base}}_{{R}}$
70 38 5 3 ringlz
71 60 69 70 syl2anc
72 59 71 sylan9eqr
73 72 ex
74 73 ex
75 74 com23
76 75 a1dd
77 76 com14
79 58 78 syld
80 79 com24
81 80 ex
82 81 com14
83 82 imp
84 83 com14
86 85 com13
87 51 86 pm2.61i
88 20 87 syl5bi
89 88 imp
90 89 impl
91 90 mpteq2dva
92 91 oveq2d
93 ringmnd ${⊢}{R}\in \mathrm{Ring}\to {R}\in \mathrm{Mnd}$
94 ovexd ${⊢}{R}\in \mathrm{Ring}\to \left(0\dots {n}\right)\in \mathrm{V}$
95 3 gsumz
96 93 94 95 syl2anc