# Metamath Proof Explorer

## Theorem coe1tmmul

Description: Coefficient vector of a polynomial multiplied on the left by a term. (Contributed by Stefan O'Rear, 29-Mar-2015)

Ref Expression
Hypotheses coe1tm.z
coe1tm.k ${⊢}{K}={\mathrm{Base}}_{{R}}$
coe1tm.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
coe1tm.x ${⊢}{X}={\mathrm{var}}_{1}\left({R}\right)$
coe1tm.m
coe1tm.n ${⊢}{N}={\mathrm{mulGrp}}_{{P}}$
coe1tm.e
coe1tmmul.b ${⊢}{B}={\mathrm{Base}}_{{P}}$
coe1tmmul.t
coe1tmmul.u
coe1tmmul.a ${⊢}{\phi }\to {A}\in {B}$
coe1tmmul.r ${⊢}{\phi }\to {R}\in \mathrm{Ring}$
coe1tmmul.c ${⊢}{\phi }\to {C}\in {K}$
coe1tmmul.d ${⊢}{\phi }\to {D}\in {ℕ}_{0}$
Assertion coe1tmmul

### Proof

Step Hyp Ref Expression
1 coe1tm.z
2 coe1tm.k ${⊢}{K}={\mathrm{Base}}_{{R}}$
3 coe1tm.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
4 coe1tm.x ${⊢}{X}={\mathrm{var}}_{1}\left({R}\right)$
5 coe1tm.m
6 coe1tm.n ${⊢}{N}={\mathrm{mulGrp}}_{{P}}$
7 coe1tm.e
8 coe1tmmul.b ${⊢}{B}={\mathrm{Base}}_{{P}}$
9 coe1tmmul.t
10 coe1tmmul.u
11 coe1tmmul.a ${⊢}{\phi }\to {A}\in {B}$
12 coe1tmmul.r ${⊢}{\phi }\to {R}\in \mathrm{Ring}$
13 coe1tmmul.c ${⊢}{\phi }\to {C}\in {K}$
14 coe1tmmul.d ${⊢}{\phi }\to {D}\in {ℕ}_{0}$
15 2 3 4 5 6 7 8 ply1tmcl
16 12 13 14 15 syl3anc
17 3 9 10 8 coe1mul
18 12 16 11 17 syl3anc
19 eqeq2
20 eqeq2
21 12 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in {ℕ}_{0}\right)\wedge {D}\le {x}\right)\to {R}\in \mathrm{Ring}$
22 ringmnd ${⊢}{R}\in \mathrm{Ring}\to {R}\in \mathrm{Mnd}$
23 21 22 syl ${⊢}\left(\left({\phi }\wedge {x}\in {ℕ}_{0}\right)\wedge {D}\le {x}\right)\to {R}\in \mathrm{Mnd}$
24 ovexd ${⊢}\left(\left({\phi }\wedge {x}\in {ℕ}_{0}\right)\wedge {D}\le {x}\right)\to \left(0\dots {x}\right)\in \mathrm{V}$
25 14 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in {ℕ}_{0}\right)\wedge {D}\le {x}\right)\to {D}\in {ℕ}_{0}$
26 simpr ${⊢}\left(\left({\phi }\wedge {x}\in {ℕ}_{0}\right)\wedge {D}\le {x}\right)\to {D}\le {x}$
27 fznn0 ${⊢}{x}\in {ℕ}_{0}\to \left({D}\in \left(0\dots {x}\right)↔\left({D}\in {ℕ}_{0}\wedge {D}\le {x}\right)\right)$
28 27 ad2antlr ${⊢}\left(\left({\phi }\wedge {x}\in {ℕ}_{0}\right)\wedge {D}\le {x}\right)\to \left({D}\in \left(0\dots {x}\right)↔\left({D}\in {ℕ}_{0}\wedge {D}\le {x}\right)\right)$
29 25 26 28 mpbir2and ${⊢}\left(\left({\phi }\wedge {x}\in {ℕ}_{0}\right)\wedge {D}\le {x}\right)\to {D}\in \left(0\dots {x}\right)$
30 12 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in {ℕ}_{0}\right)\wedge {y}\in \left(0\dots {x}\right)\right)\to {R}\in \mathrm{Ring}$
31 eqid
32 31 8 3 2 coe1f
33 16 32 syl
35 elfznn0 ${⊢}{y}\in \left(0\dots {x}\right)\to {y}\in {ℕ}_{0}$
36 ffvelrn
37 34 35 36 syl2an
38 eqid ${⊢}{\mathrm{coe}}_{1}\left({A}\right)={\mathrm{coe}}_{1}\left({A}\right)$
39 38 8 3 2 coe1f ${⊢}{A}\in {B}\to {\mathrm{coe}}_{1}\left({A}\right):{ℕ}_{0}⟶{K}$
40 11 39 syl ${⊢}{\phi }\to {\mathrm{coe}}_{1}\left({A}\right):{ℕ}_{0}⟶{K}$
41 40 adantr ${⊢}\left({\phi }\wedge {x}\in {ℕ}_{0}\right)\to {\mathrm{coe}}_{1}\left({A}\right):{ℕ}_{0}⟶{K}$
42 fznn0sub ${⊢}{y}\in \left(0\dots {x}\right)\to {x}-{y}\in {ℕ}_{0}$
43 ffvelrn ${⊢}\left({\mathrm{coe}}_{1}\left({A}\right):{ℕ}_{0}⟶{K}\wedge {x}-{y}\in {ℕ}_{0}\right)\to {\mathrm{coe}}_{1}\left({A}\right)\left({x}-{y}\right)\in {K}$
44 41 42 43 syl2an ${⊢}\left(\left({\phi }\wedge {x}\in {ℕ}_{0}\right)\wedge {y}\in \left(0\dots {x}\right)\right)\to {\mathrm{coe}}_{1}\left({A}\right)\left({x}-{y}\right)\in {K}$
45 2 10 ringcl
46 30 37 44 45 syl3anc
47 46 fmpttd
49 12 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℕ}_{0}\right)\wedge {D}\le {x}\right)\wedge {y}\in \left(\left(0\dots {x}\right)\setminus \left\{{D}\right\}\right)\right)\to {R}\in \mathrm{Ring}$
50 13 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℕ}_{0}\right)\wedge {D}\le {x}\right)\wedge {y}\in \left(\left(0\dots {x}\right)\setminus \left\{{D}\right\}\right)\right)\to {C}\in {K}$
51 14 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℕ}_{0}\right)\wedge {D}\le {x}\right)\wedge {y}\in \left(\left(0\dots {x}\right)\setminus \left\{{D}\right\}\right)\right)\to {D}\in {ℕ}_{0}$
52 eldifi ${⊢}{y}\in \left(\left(0\dots {x}\right)\setminus \left\{{D}\right\}\right)\to {y}\in \left(0\dots {x}\right)$
53 52 35 syl ${⊢}{y}\in \left(\left(0\dots {x}\right)\setminus \left\{{D}\right\}\right)\to {y}\in {ℕ}_{0}$
54 53 adantl ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℕ}_{0}\right)\wedge {D}\le {x}\right)\wedge {y}\in \left(\left(0\dots {x}\right)\setminus \left\{{D}\right\}\right)\right)\to {y}\in {ℕ}_{0}$
55 eldifsni ${⊢}{y}\in \left(\left(0\dots {x}\right)\setminus \left\{{D}\right\}\right)\to {y}\ne {D}$
56 55 necomd ${⊢}{y}\in \left(\left(0\dots {x}\right)\setminus \left\{{D}\right\}\right)\to {D}\ne {y}$
57 56 adantl ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℕ}_{0}\right)\wedge {D}\le {x}\right)\wedge {y}\in \left(\left(0\dots {x}\right)\setminus \left\{{D}\right\}\right)\right)\to {D}\ne {y}$
58 1 2 3 4 5 6 7 49 50 51 54 57 coe1tmfv2
59 58 oveq1d
60 2 10 1 ringlz
61 30 44 60 syl2anc
62 52 61 sylan2
64 59 63 eqtrd
65 64 24 suppss2
66 2 1 23 24 29 48 65 gsumpt
67 fveq2
68 oveq2 ${⊢}{y}={D}\to {x}-{y}={x}-{D}$
69 68 fveq2d ${⊢}{y}={D}\to {\mathrm{coe}}_{1}\left({A}\right)\left({x}-{y}\right)={\mathrm{coe}}_{1}\left({A}\right)\left({x}-{D}\right)$
70 67 69 oveq12d
71 eqid
72 ovex
73 70 71 72 fvmpt
74 29 73 syl
75 1 2 3 4 5 6 7 coe1tmfv1
76 12 13 14 75 syl3anc
78 77 oveq1d
79 74 78 eqtrd
80 66 79 eqtrd
81 12 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℕ}_{0}\right)\wedge ¬{D}\le {x}\right)\wedge {y}\in \left(0\dots {x}\right)\right)\to {R}\in \mathrm{Ring}$
82 13 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℕ}_{0}\right)\wedge ¬{D}\le {x}\right)\wedge {y}\in \left(0\dots {x}\right)\right)\to {C}\in {K}$
83 14 ad3antrrr ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℕ}_{0}\right)\wedge ¬{D}\le {x}\right)\wedge {y}\in \left(0\dots {x}\right)\right)\to {D}\in {ℕ}_{0}$
84 35 adantl ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℕ}_{0}\right)\wedge ¬{D}\le {x}\right)\wedge {y}\in \left(0\dots {x}\right)\right)\to {y}\in {ℕ}_{0}$
85 elfzle2 ${⊢}{y}\in \left(0\dots {x}\right)\to {y}\le {x}$
86 85 adantl ${⊢}\left(\left({\phi }\wedge {x}\in {ℕ}_{0}\right)\wedge {y}\in \left(0\dots {x}\right)\right)\to {y}\le {x}$
87 breq1 ${⊢}{D}={y}\to \left({D}\le {x}↔{y}\le {x}\right)$
88 86 87 syl5ibrcom ${⊢}\left(\left({\phi }\wedge {x}\in {ℕ}_{0}\right)\wedge {y}\in \left(0\dots {x}\right)\right)\to \left({D}={y}\to {D}\le {x}\right)$
89 88 necon3bd ${⊢}\left(\left({\phi }\wedge {x}\in {ℕ}_{0}\right)\wedge {y}\in \left(0\dots {x}\right)\right)\to \left(¬{D}\le {x}\to {D}\ne {y}\right)$
90 89 imp ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℕ}_{0}\right)\wedge {y}\in \left(0\dots {x}\right)\right)\wedge ¬{D}\le {x}\right)\to {D}\ne {y}$
91 90 an32s ${⊢}\left(\left(\left({\phi }\wedge {x}\in {ℕ}_{0}\right)\wedge ¬{D}\le {x}\right)\wedge {y}\in \left(0\dots {x}\right)\right)\to {D}\ne {y}$
92 1 2 3 4 5 6 7 81 82 83 84 91 coe1tmfv2
93 92 oveq1d
98 12 22 syl ${⊢}{\phi }\to {R}\in \mathrm{Mnd}$
99 98 ad2antrr ${⊢}\left(\left({\phi }\wedge {x}\in {ℕ}_{0}\right)\wedge ¬{D}\le {x}\right)\to {R}\in \mathrm{Mnd}$
100 ovexd ${⊢}\left(\left({\phi }\wedge {x}\in {ℕ}_{0}\right)\wedge ¬{D}\le {x}\right)\to \left(0\dots {x}\right)\in \mathrm{V}$