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=NMatR
mptcoe1matfsupp.q Q=Poly1A
mptcoe1matfsupp.l L=BaseQ
Assertion mptcoe1matfsupp NFinRRingOLINJNfinSupp0Rk0Icoe1OkJ

Proof

Step Hyp Ref Expression
1 mptcoe1matfsupp.a A=NMatR
2 mptcoe1matfsupp.q Q=Poly1A
3 mptcoe1matfsupp.l L=BaseQ
4 fvexd NFinRRingOLINJN0RV
5 eqid BaseR=BaseR
6 eqid BaseA=BaseA
7 simp2 NFinRRingOLINJNIN
8 7 adantr NFinRRingOLINJNk0IN
9 simp3 NFinRRingOLINJNJN
10 9 adantr NFinRRingOLINJNk0JN
11 simp3 NFinRRingOLOL
12 11 3ad2ant1 NFinRRingOLINJNOL
13 eqid coe1O=coe1O
14 13 3 2 6 coe1fvalcl OLk0coe1OkBaseA
15 12 14 sylan NFinRRingOLINJNk0coe1OkBaseA
16 1 5 6 8 10 15 matecld NFinRRingOLINJNk0Icoe1OkJBaseR
17 eqid 0A=0A
18 13 3 2 17 6 coe1fsupp OLcoe1OcBaseA0|finSupp0Ac
19 elrabi coe1OcBaseA0|finSupp0Accoe1OBaseA0
20 12 18 19 3syl NFinRRingOLINJNcoe1OBaseA0
21 fvex 0AV
22 20 21 jctir NFinRRingOLINJNcoe1OBaseA00AV
23 13 3 2 17 coe1sfi OLfinSupp0Acoe1O
24 12 23 syl NFinRRingOLINJNfinSupp0Acoe1O
25 fsuppmapnn0ub coe1OBaseA00AVfinSupp0Acoe1Os0x0s<xcoe1Ox=0A
26 22 24 25 sylc NFinRRingOLINJNs0x0s<xcoe1Ox=0A
27 csbov x/kIcoe1OkJ=Ix/kcoe1OkJ
28 csbfv x/kcoe1Ok=coe1Ox
29 28 oveqi Ix/kcoe1OkJ=Icoe1OxJ
30 27 29 eqtri x/kIcoe1OkJ=Icoe1OxJ
31 30 a1i NFinRRingOLINJNs0x0s<xcoe1Ox=0Ax/kIcoe1OkJ=Icoe1OxJ
32 oveq coe1Ox=0AIcoe1OxJ=I0AJ
33 32 adantl NFinRRingOLINJNs0x0s<xcoe1Ox=0AIcoe1OxJ=I0AJ
34 eqid 0R=0R
35 1 34 mat0op NFinRRing0A=iN,jN0R
36 35 3adant3 NFinRRingOL0A=iN,jN0R
37 36 3ad2ant1 NFinRRingOLINJN0A=iN,jN0R
38 eqidd NFinRRingOLINJNi=Ij=J0R=0R
39 37 38 7 9 4 ovmpod NFinRRingOLINJNI0AJ=0R
40 39 ad4antr NFinRRingOLINJNs0x0s<xcoe1Ox=0AI0AJ=0R
41 31 33 40 3eqtrd NFinRRingOLINJNs0x0s<xcoe1Ox=0Ax/kIcoe1OkJ=0R
42 41 exp31 NFinRRingOLINJNs0x0s<xcoe1Ox=0Ax/kIcoe1OkJ=0R
43 42 a2d NFinRRingOLINJNs0x0s<xcoe1Ox=0As<xx/kIcoe1OkJ=0R
44 43 ralimdva NFinRRingOLINJNs0x0s<xcoe1Ox=0Ax0s<xx/kIcoe1OkJ=0R
45 44 reximdva NFinRRingOLINJNs0x0s<xcoe1Ox=0As0x0s<xx/kIcoe1OkJ=0R
46 26 45 mpd NFinRRingOLINJNs0x0s<xx/kIcoe1OkJ=0R
47 4 16 46 mptnn0fsupp NFinRRingOLINJNfinSupp0Rk0Icoe1OkJ