# Metamath Proof Explorer

## Theorem mptcoe1matfsupp

Description: The mapping extracting the entries of the coefficient matrices of a polynomial over matrices at a fixed position is finitely supported. (Contributed by AV, 6-Oct-2019) (Proof shortened by AV, 23-Dec-2019)

Ref Expression
Hypotheses mptcoe1matfsupp.a ${⊢}{A}={N}\mathrm{Mat}{R}$
mptcoe1matfsupp.q ${⊢}{Q}={\mathrm{Poly}}_{1}\left({A}\right)$
mptcoe1matfsupp.l ${⊢}{L}={\mathrm{Base}}_{{Q}}$
Assertion mptcoe1matfsupp ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {I}\in {N}\wedge {J}\in {N}\right)\to {finSupp}_{{0}_{{R}}}\left(\left({k}\in {ℕ}_{0}⟼{I}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){J}\right)\right)$

### Proof

Step Hyp Ref Expression
1 mptcoe1matfsupp.a ${⊢}{A}={N}\mathrm{Mat}{R}$
2 mptcoe1matfsupp.q ${⊢}{Q}={\mathrm{Poly}}_{1}\left({A}\right)$
3 mptcoe1matfsupp.l ${⊢}{L}={\mathrm{Base}}_{{Q}}$
4 fvexd ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {I}\in {N}\wedge {J}\in {N}\right)\to {0}_{{R}}\in \mathrm{V}$
5 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
6 eqid ${⊢}{\mathrm{Base}}_{{A}}={\mathrm{Base}}_{{A}}$
7 simp2 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {I}\in {N}\wedge {J}\in {N}\right)\to {I}\in {N}$
8 7 adantr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {I}\in {N}\wedge {J}\in {N}\right)\wedge {k}\in {ℕ}_{0}\right)\to {I}\in {N}$
9 simp3 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {I}\in {N}\wedge {J}\in {N}\right)\to {J}\in {N}$
10 9 adantr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {I}\in {N}\wedge {J}\in {N}\right)\wedge {k}\in {ℕ}_{0}\right)\to {J}\in {N}$
11 simp3 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {O}\in {L}$
12 11 3ad2ant1 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {I}\in {N}\wedge {J}\in {N}\right)\to {O}\in {L}$
13 eqid ${⊢}{\mathrm{coe}}_{1}\left({O}\right)={\mathrm{coe}}_{1}\left({O}\right)$
14 13 3 2 6 coe1fvalcl ${⊢}\left({O}\in {L}\wedge {k}\in {ℕ}_{0}\right)\to {\mathrm{coe}}_{1}\left({O}\right)\left({k}\right)\in {\mathrm{Base}}_{{A}}$
15 12 14 sylan ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {I}\in {N}\wedge {J}\in {N}\right)\wedge {k}\in {ℕ}_{0}\right)\to {\mathrm{coe}}_{1}\left({O}\right)\left({k}\right)\in {\mathrm{Base}}_{{A}}$
16 1 5 6 8 10 15 matecld ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {I}\in {N}\wedge {J}\in {N}\right)\wedge {k}\in {ℕ}_{0}\right)\to {I}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){J}\in {\mathrm{Base}}_{{R}}$
17 eqid ${⊢}{0}_{{A}}={0}_{{A}}$
18 13 3 2 17 6 coe1fsupp ${⊢}{O}\in {L}\to {\mathrm{coe}}_{1}\left({O}\right)\in \left\{{c}\in \left({{\mathrm{Base}}_{{A}}}^{{ℕ}_{0}}\right)|{finSupp}_{{0}_{{A}}}\left({c}\right)\right\}$
19 elrabi ${⊢}{\mathrm{coe}}_{1}\left({O}\right)\in \left\{{c}\in \left({{\mathrm{Base}}_{{A}}}^{{ℕ}_{0}}\right)|{finSupp}_{{0}_{{A}}}\left({c}\right)\right\}\to {\mathrm{coe}}_{1}\left({O}\right)\in \left({{\mathrm{Base}}_{{A}}}^{{ℕ}_{0}}\right)$
20 12 18 19 3syl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {I}\in {N}\wedge {J}\in {N}\right)\to {\mathrm{coe}}_{1}\left({O}\right)\in \left({{\mathrm{Base}}_{{A}}}^{{ℕ}_{0}}\right)$
21 fvex ${⊢}{0}_{{A}}\in \mathrm{V}$
22 20 21 jctir ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {I}\in {N}\wedge {J}\in {N}\right)\to \left({\mathrm{coe}}_{1}\left({O}\right)\in \left({{\mathrm{Base}}_{{A}}}^{{ℕ}_{0}}\right)\wedge {0}_{{A}}\in \mathrm{V}\right)$
23 13 3 2 17 coe1sfi ${⊢}{O}\in {L}\to {finSupp}_{{0}_{{A}}}\left({\mathrm{coe}}_{1}\left({O}\right)\right)$
24 12 23 syl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {I}\in {N}\wedge {J}\in {N}\right)\to {finSupp}_{{0}_{{A}}}\left({\mathrm{coe}}_{1}\left({O}\right)\right)$
25 fsuppmapnn0ub ${⊢}\left({\mathrm{coe}}_{1}\left({O}\right)\in \left({{\mathrm{Base}}_{{A}}}^{{ℕ}_{0}}\right)\wedge {0}_{{A}}\in \mathrm{V}\right)\to \left({finSupp}_{{0}_{{A}}}\left({\mathrm{coe}}_{1}\left({O}\right)\right)\to \exists {s}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\right)$
26 22 24 25 sylc ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {I}\in {N}\wedge {J}\in {N}\right)\to \exists {s}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({s}<{x}\to {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)$
27 csbov
28 csbfv
29 28 oveqi
30 27 29 eqtri
31 30 a1i
32 oveq ${⊢}{\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\to {I}{\mathrm{coe}}_{1}\left({O}\right)\left({x}\right){J}={I}{0}_{{A}}{J}$
33 32 adantl ${⊢}\left(\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {I}\in {N}\wedge {J}\in {N}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge {x}\in {ℕ}_{0}\right)\wedge {s}<{x}\right)\wedge {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\to {I}{\mathrm{coe}}_{1}\left({O}\right)\left({x}\right){J}={I}{0}_{{A}}{J}$
34 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
35 1 34 mat0op ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {0}_{{A}}=\left({i}\in {N},{j}\in {N}⟼{0}_{{R}}\right)$
36 35 3adant3 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\to {0}_{{A}}=\left({i}\in {N},{j}\in {N}⟼{0}_{{R}}\right)$
37 36 3ad2ant1 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {I}\in {N}\wedge {J}\in {N}\right)\to {0}_{{A}}=\left({i}\in {N},{j}\in {N}⟼{0}_{{R}}\right)$
38 eqidd ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {I}\in {N}\wedge {J}\in {N}\right)\wedge \left({i}={I}\wedge {j}={J}\right)\right)\to {0}_{{R}}={0}_{{R}}$
39 37 38 7 9 4 ovmpod ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {I}\in {N}\wedge {J}\in {N}\right)\to {I}{0}_{{A}}{J}={0}_{{R}}$
40 39 ad4antr ${⊢}\left(\left(\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {I}\in {N}\wedge {J}\in {N}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge {x}\in {ℕ}_{0}\right)\wedge {s}<{x}\right)\wedge {\mathrm{coe}}_{1}\left({O}\right)\left({x}\right)={0}_{{A}}\right)\to {I}{0}_{{A}}{J}={0}_{{R}}$
41 31 33 40 3eqtrd
42 41 exp31
43 42 a2d
44 43 ralimdva
45 44 reximdva
46 26 45 mpd
47 4 16 46 mptnn0fsupp ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {O}\in {L}\right)\wedge {I}\in {N}\wedge {J}\in {N}\right)\to {finSupp}_{{0}_{{R}}}\left(\left({k}\in {ℕ}_{0}⟼{I}{\mathrm{coe}}_{1}\left({O}\right)\left({k}\right){J}\right)\right)$