# Metamath Proof Explorer

## Theorem pm2mpcl

Description: The transformation of polynomial matrices into polynomials over matrices maps polynomial matrices to polynomials over matrices. (Contributed by AV, 5-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}$
pm2mpcl.l ${⊢}{L}={\mathrm{Base}}_{{Q}}$
Assertion pm2mpcl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {T}\left({M}\right)\in {L}$

### 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 pm2mpcl.l ${⊢}{L}={\mathrm{Base}}_{{Q}}$
11 1 2 3 4 5 6 7 8 9 pm2mpfval
12 eqid ${⊢}{0}_{{Q}}={0}_{{Q}}$
13 7 matring ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {A}\in \mathrm{Ring}$
14 8 ply1ring ${⊢}{A}\in \mathrm{Ring}\to {Q}\in \mathrm{Ring}$
15 ringcmn ${⊢}{Q}\in \mathrm{Ring}\to {Q}\in \mathrm{CMnd}$
16 13 14 15 3syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {Q}\in \mathrm{CMnd}$
17 16 3adant3 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {Q}\in \mathrm{CMnd}$
18 nn0ex ${⊢}{ℕ}_{0}\in \mathrm{V}$
19 18 a1i ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {ℕ}_{0}\in \mathrm{V}$
20 13 3adant3 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {A}\in \mathrm{Ring}$
21 20 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge {k}\in {ℕ}_{0}\right)\to {A}\in \mathrm{Ring}$
22 simpl2 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge {k}\in {ℕ}_{0}\right)\to {R}\in \mathrm{Ring}$
23 simpl3 ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge {k}\in {ℕ}_{0}\right)\to {M}\in {B}$
24 simpr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge {k}\in {ℕ}_{0}\right)\to {k}\in {ℕ}_{0}$
25 eqid ${⊢}{\mathrm{Base}}_{{A}}={\mathrm{Base}}_{{A}}$
26 1 2 3 7 25 decpmatcl ${⊢}\left({R}\in \mathrm{Ring}\wedge {M}\in {B}\wedge {k}\in {ℕ}_{0}\right)\to {M}\mathrm{decompPMat}{k}\in {\mathrm{Base}}_{{A}}$
27 22 23 24 26 syl3anc ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\wedge {k}\in {ℕ}_{0}\right)\to {M}\mathrm{decompPMat}{k}\in {\mathrm{Base}}_{{A}}$
28 eqid ${⊢}{\mathrm{mulGrp}}_{{Q}}={\mathrm{mulGrp}}_{{Q}}$
29 25 8 6 4 28 5 10 ply1tmcl
30 21 27 24 29 syl3anc
31 30 fmpttd
32 8 ply1lmod ${⊢}{A}\in \mathrm{Ring}\to {Q}\in \mathrm{LMod}$
33 20 32 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {Q}\in \mathrm{LMod}$
34 eqidd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to \mathrm{Scalar}\left({Q}\right)=\mathrm{Scalar}\left({Q}\right)$
35 8 6 28 5 10 ply1moncl
36 20 35 sylan
37 eqid ${⊢}{0}_{\mathrm{Scalar}\left({Q}\right)}={0}_{\mathrm{Scalar}\left({Q}\right)}$
38 eqid ${⊢}{0}_{{A}}={0}_{{A}}$
39 1 2 3 7 38 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)$
40 39 3adant1 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {finSupp}_{{0}_{{A}}}\left(\left({k}\in {ℕ}_{0}⟼{M}\mathrm{decompPMat}{k}\right)\right)$
41 8 ply1sca ${⊢}{A}\in \mathrm{Ring}\to {A}=\mathrm{Scalar}\left({Q}\right)$
42 41 eqcomd ${⊢}{A}\in \mathrm{Ring}\to \mathrm{Scalar}\left({Q}\right)={A}$
43 20 42 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to \mathrm{Scalar}\left({Q}\right)={A}$
44 43 fveq2d ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {0}_{\mathrm{Scalar}\left({Q}\right)}={0}_{{A}}$
45 40 44 breqtrrd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {finSupp}_{{0}_{\mathrm{Scalar}\left({Q}\right)}}\left(\left({k}\in {ℕ}_{0}⟼{M}\mathrm{decompPMat}{k}\right)\right)$
46 19 33 34 10 27 36 12 37 4 45 mptscmfsupp0
47 10 12 17 19 31 46 gsumcl
48 11 47 eqeltrd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\wedge {M}\in {B}\right)\to {T}\left({M}\right)\in {L}$