# Metamath Proof Explorer

## Theorem pmatcoe1fsupp

Description: For a polynomial matrix there is an upper bound for the coefficients of all the polynomials being not 0. (Contributed by AV, 3-Oct-2019) (Proof shortened by AV, 28-Nov-2019)

Ref Expression
Hypotheses pmatcoe1fsupp.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
pmatcoe1fsupp.c ${⊢}{C}={N}\mathrm{Mat}{P}$
pmatcoe1fsupp.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
pmatcoe1fsupp.0
Assertion pmatcoe1fsupp

### Proof

Step Hyp Ref Expression
1 pmatcoe1fsupp.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
2 pmatcoe1fsupp.c ${⊢}{C}={N}\mathrm{Mat}{P}$
3 pmatcoe1fsupp.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
4 pmatcoe1fsupp.0
5 ssrab2
6 5 a1i
7 6 olcd
8 inss
9 7 8 syl
10 xpfi ${⊢}\left({N}\in \mathrm{Fin}\wedge {N}\in \mathrm{Fin}\right)\to {N}×{N}\in \mathrm{Fin}$
11 10 anidms ${⊢}{N}\in \mathrm{Fin}\to {N}×{N}\in \mathrm{Fin}$
12 snfi ${⊢}\left\{{\mathrm{coe}}_{1}\left({M}\left({u}\right)\right)\right\}\in \mathrm{Fin}$
13 12 a1i ${⊢}\left({N}\in \mathrm{Fin}\wedge {u}\in \left({N}×{N}\right)\right)\to \left\{{\mathrm{coe}}_{1}\left({M}\left({u}\right)\right)\right\}\in \mathrm{Fin}$
14 13 ralrimiva ${⊢}{N}\in \mathrm{Fin}\to \forall {u}\in \left({N}×{N}\right)\phantom{\rule{.4em}{0ex}}\left\{{\mathrm{coe}}_{1}\left({M}\left({u}\right)\right)\right\}\in \mathrm{Fin}$
15 11 14 jca ${⊢}{N}\in \mathrm{Fin}\to \left({N}×{N}\in \mathrm{Fin}\wedge \forall {u}\in \left({N}×{N}\right)\phantom{\rule{.4em}{0ex}}\left\{{\mathrm{coe}}_{1}\left({M}\left({u}\right)\right)\right\}\in \mathrm{Fin}\right)$
16 15 3ad2ant1 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to \left({N}×{N}\in \mathrm{Fin}\wedge \forall {u}\in \left({N}×{N}\right)\phantom{\rule{.4em}{0ex}}\left\{{\mathrm{coe}}_{1}\left({M}\left({u}\right)\right)\right\}\in \mathrm{Fin}\right)$
17 iunfi ${⊢}\left({N}×{N}\in \mathrm{Fin}\wedge \forall {u}\in \left({N}×{N}\right)\phantom{\rule{.4em}{0ex}}\left\{{\mathrm{coe}}_{1}\left({M}\left({u}\right)\right)\right\}\in \mathrm{Fin}\right)\to \bigcup _{{u}\in {N}×{N}}\left\{{\mathrm{coe}}_{1}\left({M}\left({u}\right)\right)\right\}\in \mathrm{Fin}$
18 infi
19 16 17 18 3syl
20 fvex ${⊢}{0}_{{R}}\in \mathrm{V}$
21 4 20 eqeltri
22 21 a1i
23 elin
24 breq1
25 24 elrab
26 25 simprbi
27 23 26 simplbiim
28 27 rgen
29 28 a1i
30 fsuppmapnn0fiub0
31 30 imp
32 9 19 22 29 31 syl31anc
33 opelxpi ${⊢}\left({i}\in {N}\wedge {j}\in {N}\right)\to ⟨{i},{j}⟩\in \left({N}×{N}\right)$
34 df-ov ${⊢}{i}{M}{j}={M}\left(⟨{i},{j}⟩\right)$
35 34 fveq2i ${⊢}{\mathrm{coe}}_{1}\left({i}{M}{j}\right)={\mathrm{coe}}_{1}\left({M}\left(⟨{i},{j}⟩\right)\right)$
36 fvex ${⊢}{\mathrm{coe}}_{1}\left({M}\left(⟨{i},{j}⟩\right)\right)\in \mathrm{V}$
37 36 snid ${⊢}{\mathrm{coe}}_{1}\left({M}\left(⟨{i},{j}⟩\right)\right)\in \left\{{\mathrm{coe}}_{1}\left({M}\left(⟨{i},{j}⟩\right)\right)\right\}$
38 35 37 eqeltri ${⊢}{\mathrm{coe}}_{1}\left({i}{M}{j}\right)\in \left\{{\mathrm{coe}}_{1}\left({M}\left(⟨{i},{j}⟩\right)\right)\right\}$
39 38 a1i ${⊢}\left({i}\in {N}\wedge {j}\in {N}\right)\to {\mathrm{coe}}_{1}\left({i}{M}{j}\right)\in \left\{{\mathrm{coe}}_{1}\left({M}\left(⟨{i},{j}⟩\right)\right)\right\}$
40 2fveq3 ${⊢}{u}=⟨{i},{j}⟩\to {\mathrm{coe}}_{1}\left({M}\left({u}\right)\right)={\mathrm{coe}}_{1}\left({M}\left(⟨{i},{j}⟩\right)\right)$
41 40 sneqd ${⊢}{u}=⟨{i},{j}⟩\to \left\{{\mathrm{coe}}_{1}\left({M}\left({u}\right)\right)\right\}=\left\{{\mathrm{coe}}_{1}\left({M}\left(⟨{i},{j}⟩\right)\right)\right\}$
42 41 eliuni ${⊢}\left(⟨{i},{j}⟩\in \left({N}×{N}\right)\wedge {\mathrm{coe}}_{1}\left({i}{M}{j}\right)\in \left\{{\mathrm{coe}}_{1}\left({M}\left(⟨{i},{j}⟩\right)\right)\right\}\right)\to {\mathrm{coe}}_{1}\left({i}{M}{j}\right)\in \bigcup _{{u}\in {N}×{N}}\left\{{\mathrm{coe}}_{1}\left({M}\left({u}\right)\right)\right\}$
43 33 39 42 syl2anc ${⊢}\left({i}\in {N}\wedge {j}\in {N}\right)\to {\mathrm{coe}}_{1}\left({i}{M}{j}\right)\in \bigcup _{{u}\in {N}×{N}}\left\{{\mathrm{coe}}_{1}\left({M}\left({u}\right)\right)\right\}$
44 43 adantl ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge {x}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {\mathrm{coe}}_{1}\left({i}{M}{j}\right)\in \bigcup _{{u}\in {N}×{N}}\left\{{\mathrm{coe}}_{1}\left({M}\left({u}\right)\right)\right\}$
45 eqid ${⊢}{\mathrm{Base}}_{{P}}={\mathrm{Base}}_{{P}}$
46 simprl ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge {x}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {i}\in {N}$
47 simprr ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge {x}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {j}\in {N}$
48 3 eleq2i ${⊢}{M}\in {B}↔{M}\in {\mathrm{Base}}_{{C}}$
49 48 biimpi ${⊢}{M}\in {B}\to {M}\in {\mathrm{Base}}_{{C}}$
50 49 3ad2ant3 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {M}\in {\mathrm{Base}}_{{C}}$
51 50 ad3antrrr ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge {x}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {M}\in {\mathrm{Base}}_{{C}}$
52 51 3 eleqtrrdi ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge {x}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {M}\in {B}$
53 2 45 3 46 47 52 matecld ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge {x}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {i}{M}{j}\in {\mathrm{Base}}_{{P}}$
54 eqid ${⊢}{\mathrm{coe}}_{1}\left({i}{M}{j}\right)={\mathrm{coe}}_{1}\left({i}{M}{j}\right)$
55 eqid ${⊢}{0}_{{R}}={0}_{{R}}$
56 eqid ${⊢}{\mathrm{Base}}_{{R}}={\mathrm{Base}}_{{R}}$
57 54 45 1 55 56 coe1fsupp ${⊢}{i}{M}{j}\in {\mathrm{Base}}_{{P}}\to {\mathrm{coe}}_{1}\left({i}{M}{j}\right)\in \left\{{v}\in \left({{\mathrm{Base}}_{{R}}}^{{ℕ}_{0}}\right)|{finSupp}_{{0}_{{R}}}\left({v}\right)\right\}$
58 53 57 syl ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge {x}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {\mathrm{coe}}_{1}\left({i}{M}{j}\right)\in \left\{{v}\in \left({{\mathrm{Base}}_{{R}}}^{{ℕ}_{0}}\right)|{finSupp}_{{0}_{{R}}}\left({v}\right)\right\}$
59 4 a1i
60 59 breq2d
61 60 rabbidv
62 61 eleq2d
63 62 ad3antrrr
64 58 63 mpbird
65 44 64 elind
66 simplr ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge {s}\in {ℕ}_{0}\right)\wedge {x}\in {ℕ}_{0}\right)\wedge \left({i}\in {N}\wedge {j}\in {N}\right)\right)\to {x}\in {ℕ}_{0}$
67 fveq1 ${⊢}{w}={\mathrm{coe}}_{1}\left({i}{M}{j}\right)\to {w}\left({z}\right)={\mathrm{coe}}_{1}\left({i}{M}{j}\right)\left({z}\right)$
68 67 eqeq1d
69 68 imbi2d
70 breq2 ${⊢}{z}={x}\to \left({s}<{z}↔{s}<{x}\right)$
71 fveqeq2
72 70 71 imbi12d
73 69 72 rspc2v
74 65 66 73 syl2anc
75 74 ex
76 75 com23
77 76 impancom
78 77 imp
79 78 com23
80 79 ralrimdvv
81 80 ralrimiva
82 81 ex
83 82 reximdva
84 32 83 mpd