# Metamath Proof Explorer

## Theorem pm2mpcoe1

Description: A coefficient of the polynomial over matrices which is the result of the transformation of a polynomial matrix is the matrix consisting of the coefficients in the polynomial entries of the polynomial matrix. (Contributed by AV, 20-Oct-2019) (Revised by AV, 5-Dec-2019)

Ref Expression
Hypotheses pm2mpval.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
pm2mpval.c ${⊢}{C}={N}\mathrm{Mat}{P}$
pm2mpval.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
pm2mpval.m
pm2mpval.e
pm2mpval.x ${⊢}{X}={\mathrm{var}}_{1}\left({A}\right)$
pm2mpval.a ${⊢}{A}={N}\mathrm{Mat}{R}$
pm2mpval.q ${⊢}{Q}={\mathrm{Poly}}_{1}\left({A}\right)$
pm2mpval.t ${⊢}{T}={N}\mathrm{pMatToMatPoly}{R}$
Assertion pm2mpcoe1 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({M}\in {B}\wedge {K}\in {ℕ}_{0}\right)\right)\to {\mathrm{coe}}_{1}\left({T}\left({M}\right)\right)\left({K}\right)={M}\mathrm{decompPMat}{K}$

### Proof

Step Hyp Ref Expression
1 pm2mpval.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
2 pm2mpval.c ${⊢}{C}={N}\mathrm{Mat}{P}$
3 pm2mpval.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
4 pm2mpval.m
5 pm2mpval.e
6 pm2mpval.x ${⊢}{X}={\mathrm{var}}_{1}\left({A}\right)$
7 pm2mpval.a ${⊢}{A}={N}\mathrm{Mat}{R}$
8 pm2mpval.q ${⊢}{Q}={\mathrm{Poly}}_{1}\left({A}\right)$
9 pm2mpval.t ${⊢}{T}={N}\mathrm{pMatToMatPoly}{R}$
10 simpll ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({M}\in {B}\wedge {K}\in {ℕ}_{0}\right)\right)\to {N}\in \mathrm{Fin}$
11 simplr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({M}\in {B}\wedge {K}\in {ℕ}_{0}\right)\right)\to {R}\in \mathrm{Ring}$
12 simprl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({M}\in {B}\wedge {K}\in {ℕ}_{0}\right)\right)\to {M}\in {B}$
13 1 2 3 4 5 6 7 8 9 pm2mpfval
14 10 11 12 13 syl3anc
15 14 fveq2d
16 15 fveq1d
17 eqid ${⊢}{\mathrm{Base}}_{{Q}}={\mathrm{Base}}_{{Q}}$
18 7 matring ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {A}\in \mathrm{Ring}$
19 18 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({M}\in {B}\wedge {K}\in {ℕ}_{0}\right)\right)\to {A}\in \mathrm{Ring}$
20 eqid ${⊢}{\mathrm{Base}}_{{A}}={\mathrm{Base}}_{{A}}$
21 eqid ${⊢}{0}_{{A}}={0}_{{A}}$
22 11 adantr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({M}\in {B}\wedge {K}\in {ℕ}_{0}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to {R}\in \mathrm{Ring}$
23 12 adantr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({M}\in {B}\wedge {K}\in {ℕ}_{0}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to {M}\in {B}$
24 simpr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({M}\in {B}\wedge {K}\in {ℕ}_{0}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to {k}\in {ℕ}_{0}$
25 1 2 3 7 20 decpmatcl ${⊢}\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\wedge {k}\in {ℕ}_{0}\right)\to {M}\mathrm{decompPMat}{k}\in {\mathrm{Base}}_{{A}}$
26 22 23 24 25 syl3anc ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({M}\in {B}\wedge {K}\in {ℕ}_{0}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to {M}\mathrm{decompPMat}{k}\in {\mathrm{Base}}_{{A}}$
27 26 ralrimiva ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({M}\in {B}\wedge {K}\in {ℕ}_{0}\right)\right)\to \forall {k}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}{M}\mathrm{decompPMat}{k}\in {\mathrm{Base}}_{{A}}$
28 1 2 3 7 21 decpmatfsupp ${⊢}\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {finSupp}_{{0}_{{A}}}\left(\left({k}\in {ℕ}_{0}⟼{M}\mathrm{decompPMat}{k}\right)\right)$
29 28 ad2ant2lr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({M}\in {B}\wedge {K}\in {ℕ}_{0}\right)\right)\to {finSupp}_{{0}_{{A}}}\left(\left({k}\in {ℕ}_{0}⟼{M}\mathrm{decompPMat}{k}\right)\right)$
30 simpr ${⊢}\left({M}\in {B}\wedge {K}\in {ℕ}_{0}\right)\to {K}\in {ℕ}_{0}$
31 30 adantl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({M}\in {B}\wedge {K}\in {ℕ}_{0}\right)\right)\to {K}\in {ℕ}_{0}$
32 8 17 6 5 19 20 4 21 27 29 31 gsummoncoe1
33 csbov2g
34 csbvarg
35 34 oveq2d
36 33 35 eqtrd
39 16 32 38 3eqtrd ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({M}\in {B}\wedge {K}\in {ℕ}_{0}\right)\right)\to {\mathrm{coe}}_{1}\left({T}\left({M}\right)\right)\left({K}\right)={M}\mathrm{decompPMat}{K}$