# Metamath Proof Explorer

## Theorem pm2mp

Description: The transformation of a sum of matrices having scaled monomials with the same power as entries into a sum of scaled monomials as a polynomial over matrices. (Contributed by AV, 12-Nov-2019) (Revised by AV, 7-Dec-2019)

Ref Expression
Hypotheses monmat2matmon.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
monmat2matmon.c ${⊢}{C}={N}\mathrm{Mat}{P}$
monmat2matmon.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
monmat2matmon.m1
monmat2matmon.e1
monmat2matmon.x ${⊢}{X}={\mathrm{var}}_{1}\left({A}\right)$
monmat2matmon.a ${⊢}{A}={N}\mathrm{Mat}{R}$
monmat2matmon.k ${⊢}{K}={\mathrm{Base}}_{{A}}$
monmat2matmon.q ${⊢}{Q}={\mathrm{Poly}}_{1}\left({A}\right)$
monmat2matmon.i ${⊢}{I}={N}\mathrm{pMatToMatPoly}{R}$
monmat2matmon.e2 ${⊢}{E}={\cdot }_{{\mathrm{mulGrp}}_{{P}}}$
monmat2matmon.y ${⊢}{Y}={\mathrm{var}}_{1}\left({R}\right)$
monmat2matmon.m2
monmat2matmon.t ${⊢}{T}={N}\mathrm{matToPolyMat}{R}$
Assertion pm2mp

### Proof

Step Hyp Ref Expression
1 monmat2matmon.p ${⊢}{P}={\mathrm{Poly}}_{1}\left({R}\right)$
2 monmat2matmon.c ${⊢}{C}={N}\mathrm{Mat}{P}$
3 monmat2matmon.b ${⊢}{B}={\mathrm{Base}}_{{C}}$
4 monmat2matmon.m1
5 monmat2matmon.e1
6 monmat2matmon.x ${⊢}{X}={\mathrm{var}}_{1}\left({A}\right)$
7 monmat2matmon.a ${⊢}{A}={N}\mathrm{Mat}{R}$
8 monmat2matmon.k ${⊢}{K}={\mathrm{Base}}_{{A}}$
9 monmat2matmon.q ${⊢}{Q}={\mathrm{Poly}}_{1}\left({A}\right)$
10 monmat2matmon.i ${⊢}{I}={N}\mathrm{pMatToMatPoly}{R}$
11 monmat2matmon.e2 ${⊢}{E}={\cdot }_{{\mathrm{mulGrp}}_{{P}}}$
12 monmat2matmon.y ${⊢}{Y}={\mathrm{var}}_{1}\left({R}\right)$
13 monmat2matmon.m2
14 monmat2matmon.t ${⊢}{T}={N}\mathrm{matToPolyMat}{R}$
15 eqid ${⊢}{0}_{{C}}={0}_{{C}}$
16 crngring ${⊢}{R}\in \mathrm{CRing}\to {R}\in \mathrm{Ring}$
17 16 anim2i ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)$
18 1 2 pmatring ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {C}\in \mathrm{Ring}$
19 ringcmn ${⊢}{C}\in \mathrm{Ring}\to {C}\in \mathrm{CMnd}$
20 17 18 19 3syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {C}\in \mathrm{CMnd}$
21 20 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in \left({{K}}^{{ℕ}_{0}}\right)\wedge {finSupp}_{{0}_{{A}}}\left({M}\right)\right)\right)\to {C}\in \mathrm{CMnd}$
22 7 matring ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {A}\in \mathrm{Ring}$
23 16 22 sylan2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {A}\in \mathrm{Ring}$
24 9 ply1ring ${⊢}{A}\in \mathrm{Ring}\to {Q}\in \mathrm{Ring}$
25 ringmnd ${⊢}{Q}\in \mathrm{Ring}\to {Q}\in \mathrm{Mnd}$
26 23 24 25 3syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {Q}\in \mathrm{Mnd}$
27 26 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in \left({{K}}^{{ℕ}_{0}}\right)\wedge {finSupp}_{{0}_{{A}}}\left({M}\right)\right)\right)\to {Q}\in \mathrm{Mnd}$
28 nn0ex ${⊢}{ℕ}_{0}\in \mathrm{V}$
29 28 a1i ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in \left({{K}}^{{ℕ}_{0}}\right)\wedge {finSupp}_{{0}_{{A}}}\left({M}\right)\right)\right)\to {ℕ}_{0}\in \mathrm{V}$
30 eqid ${⊢}{\mathrm{Base}}_{{Q}}={\mathrm{Base}}_{{Q}}$
31 1 2 3 4 5 6 7 9 30 10 pm2mpghm ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {I}\in \left({C}\mathrm{GrpHom}{Q}\right)$
32 16 31 sylan2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {I}\in \left({C}\mathrm{GrpHom}{Q}\right)$
33 32 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in \left({{K}}^{{ℕ}_{0}}\right)\wedge {finSupp}_{{0}_{{A}}}\left({M}\right)\right)\right)\to {I}\in \left({C}\mathrm{GrpHom}{Q}\right)$
34 ghmmhm ${⊢}{I}\in \left({C}\mathrm{GrpHom}{Q}\right)\to {I}\in \left({C}\mathrm{MndHom}{Q}\right)$
35 33 34 syl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in \left({{K}}^{{ℕ}_{0}}\right)\wedge {finSupp}_{{0}_{{A}}}\left({M}\right)\right)\right)\to {I}\in \left({C}\mathrm{MndHom}{Q}\right)$
36 17 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in \left({{K}}^{{ℕ}_{0}}\right)\wedge {finSupp}_{{0}_{{A}}}\left({M}\right)\right)\right)\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)$
37 36 adantr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in \left({{K}}^{{ℕ}_{0}}\right)\wedge {finSupp}_{{0}_{{A}}}\left({M}\right)\right)\right)\wedge {n}\in {ℕ}_{0}\right)\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)$
38 elmapi ${⊢}{M}\in \left({{K}}^{{ℕ}_{0}}\right)\to {M}:{ℕ}_{0}⟶{K}$
39 38 adantr ${⊢}\left({M}\in \left({{K}}^{{ℕ}_{0}}\right)\wedge {finSupp}_{{0}_{{A}}}\left({M}\right)\right)\to {M}:{ℕ}_{0}⟶{K}$
40 39 adantl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in \left({{K}}^{{ℕ}_{0}}\right)\wedge {finSupp}_{{0}_{{A}}}\left({M}\right)\right)\right)\to {M}:{ℕ}_{0}⟶{K}$
41 40 ffvelrnda ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in \left({{K}}^{{ℕ}_{0}}\right)\wedge {finSupp}_{{0}_{{A}}}\left({M}\right)\right)\right)\wedge {n}\in {ℕ}_{0}\right)\to {M}\left({n}\right)\in {K}$
42 simpr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in \left({{K}}^{{ℕ}_{0}}\right)\wedge {finSupp}_{{0}_{{A}}}\left({M}\right)\right)\right)\wedge {n}\in {ℕ}_{0}\right)\to {n}\in {ℕ}_{0}$
43 7 8 14 1 2 3 13 11 12 mat2pmatscmxcl
44 37 41 42 43 syl12anc
45 fvexd ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in \left({{K}}^{{ℕ}_{0}}\right)\wedge {finSupp}_{{0}_{{A}}}\left({M}\right)\right)\right)\to {0}_{{C}}\in \mathrm{V}$
46 ovexd
47 simpr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge {M}\in \left({{K}}^{{ℕ}_{0}}\right)\right)\to {M}\in \left({{K}}^{{ℕ}_{0}}\right)$
48 fvex ${⊢}{0}_{{A}}\in \mathrm{V}$
49 fsuppmapnn0ub ${⊢}\left({M}\in \left({{K}}^{{ℕ}_{0}}\right)\wedge {0}_{{A}}\in \mathrm{V}\right)\to \left({finSupp}_{{0}_{{A}}}\left({M}\right)\to \exists {y}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to {M}\left({x}\right)={0}_{{A}}\right)\right)$
50 47 48 49 sylancl ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge {M}\in \left({{K}}^{{ℕ}_{0}}\right)\right)\to \left({finSupp}_{{0}_{{A}}}\left({M}\right)\to \exists {y}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\forall {x}\in {ℕ}_{0}\phantom{\rule{.4em}{0ex}}\left({y}<{x}\to {M}\left({x}\right)={0}_{{A}}\right)\right)$
51 csbov12g
52 csbov1g
53 csbvarg
54 53 oveq1d
55 52 54 eqtrd
56 csbfv2g
57 csbfv2g
58 53 fveq2d
59 57 58 eqtrd
60 59 fveq2d
61 56 60 eqtrd
62 55 61 oveq12d
63 51 62 eqtrd
66 fveq2 ${⊢}{M}\left({x}\right)={0}_{{A}}\to {T}\left({M}\left({x}\right)\right)={T}\left({0}_{{A}}\right)$
67 66 oveq2d
68 14 7 8 1 2 3 mat2pmatghm ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {T}\in \left({A}\mathrm{GrpHom}{C}\right)$
69 16 68 sylan2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {T}\in \left({A}\mathrm{GrpHom}{C}\right)$
70 69 ad3antrrr ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge {M}\in \left({{K}}^{{ℕ}_{0}}\right)\right)\wedge {y}\in {ℕ}_{0}\right)\wedge {x}\in {ℕ}_{0}\right)\to {T}\in \left({A}\mathrm{GrpHom}{C}\right)$
71 ghmmhm ${⊢}{T}\in \left({A}\mathrm{GrpHom}{C}\right)\to {T}\in \left({A}\mathrm{MndHom}{C}\right)$
72 eqid ${⊢}{0}_{{A}}={0}_{{A}}$
73 72 15 mhm0 ${⊢}{T}\in \left({A}\mathrm{MndHom}{C}\right)\to {T}\left({0}_{{A}}\right)={0}_{{C}}$
74 70 71 73 3syl ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge {M}\in \left({{K}}^{{ℕ}_{0}}\right)\right)\wedge {y}\in {ℕ}_{0}\right)\wedge {x}\in {ℕ}_{0}\right)\to {T}\left({0}_{{A}}\right)={0}_{{C}}$
75 74 oveq2d
76 1 ply1ring ${⊢}{R}\in \mathrm{Ring}\to {P}\in \mathrm{Ring}$
77 16 76 syl ${⊢}{R}\in \mathrm{CRing}\to {P}\in \mathrm{Ring}$
78 2 matlmod ${⊢}\left({N}\in \mathrm{Fin}\wedge {P}\in \mathrm{Ring}\right)\to {C}\in \mathrm{LMod}$
79 77 78 sylan2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {C}\in \mathrm{LMod}$
80 79 ad3antrrr ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge {M}\in \left({{K}}^{{ℕ}_{0}}\right)\right)\wedge {y}\in {ℕ}_{0}\right)\wedge {x}\in {ℕ}_{0}\right)\to {C}\in \mathrm{LMod}$
81 77 adantl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {P}\in \mathrm{Ring}$
82 eqid ${⊢}{\mathrm{mulGrp}}_{{P}}={\mathrm{mulGrp}}_{{P}}$
83 82 ringmgp ${⊢}{P}\in \mathrm{Ring}\to {\mathrm{mulGrp}}_{{P}}\in \mathrm{Mnd}$
84 81 83 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {\mathrm{mulGrp}}_{{P}}\in \mathrm{Mnd}$
85 84 ad3antrrr ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge {M}\in \left({{K}}^{{ℕ}_{0}}\right)\right)\wedge {y}\in {ℕ}_{0}\right)\wedge {x}\in {ℕ}_{0}\right)\to {\mathrm{mulGrp}}_{{P}}\in \mathrm{Mnd}$
86 simpr ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge {M}\in \left({{K}}^{{ℕ}_{0}}\right)\right)\wedge {y}\in {ℕ}_{0}\right)\wedge {x}\in {ℕ}_{0}\right)\to {x}\in {ℕ}_{0}$
87 16 adantl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {R}\in \mathrm{Ring}$
88 eqid ${⊢}{\mathrm{Base}}_{{P}}={\mathrm{Base}}_{{P}}$
89 12 1 88 vr1cl ${⊢}{R}\in \mathrm{Ring}\to {Y}\in {\mathrm{Base}}_{{P}}$
90 87 89 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {Y}\in {\mathrm{Base}}_{{P}}$
91 90 ad3antrrr ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge {M}\in \left({{K}}^{{ℕ}_{0}}\right)\right)\wedge {y}\in {ℕ}_{0}\right)\wedge {x}\in {ℕ}_{0}\right)\to {Y}\in {\mathrm{Base}}_{{P}}$
92 82 88 mgpbas ${⊢}{\mathrm{Base}}_{{P}}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{P}}}$
93 92 11 mulgnn0cl ${⊢}\left({\mathrm{mulGrp}}_{{P}}\in \mathrm{Mnd}\wedge {x}\in {ℕ}_{0}\wedge {Y}\in {\mathrm{Base}}_{{P}}\right)\to {x}{E}{Y}\in {\mathrm{Base}}_{{P}}$
94 85 86 91 93 syl3anc ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge {M}\in \left({{K}}^{{ℕ}_{0}}\right)\right)\wedge {y}\in {ℕ}_{0}\right)\wedge {x}\in {ℕ}_{0}\right)\to {x}{E}{Y}\in {\mathrm{Base}}_{{P}}$
95 1 ply1crng ${⊢}{R}\in \mathrm{CRing}\to {P}\in \mathrm{CRing}$
96 2 matsca2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {P}\in \mathrm{CRing}\right)\to {P}=\mathrm{Scalar}\left({C}\right)$
97 95 96 sylan2 ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to {P}=\mathrm{Scalar}\left({C}\right)$
98 97 eqcomd ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to \mathrm{Scalar}\left({C}\right)={P}$
99 98 ad3antrrr ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge {M}\in \left({{K}}^{{ℕ}_{0}}\right)\right)\wedge {y}\in {ℕ}_{0}\right)\wedge {x}\in {ℕ}_{0}\right)\to \mathrm{Scalar}\left({C}\right)={P}$
100 99 fveq2d ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge {M}\in \left({{K}}^{{ℕ}_{0}}\right)\right)\wedge {y}\in {ℕ}_{0}\right)\wedge {x}\in {ℕ}_{0}\right)\to {\mathrm{Base}}_{\mathrm{Scalar}\left({C}\right)}={\mathrm{Base}}_{{P}}$
101 94 100 eleqtrrd ${⊢}\left(\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge {M}\in \left({{K}}^{{ℕ}_{0}}\right)\right)\wedge {y}\in {ℕ}_{0}\right)\wedge {x}\in {ℕ}_{0}\right)\to {x}{E}{Y}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({C}\right)}$
102 eqid ${⊢}\mathrm{Scalar}\left({C}\right)=\mathrm{Scalar}\left({C}\right)$
103 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({C}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({C}\right)}$
104 102 13 103 15 lmodvs0
105 80 101 104 syl2anc
106 75 105 eqtrd
107 67 106 sylan9eqr
108 65 107 eqtrd
109 108 ex
110 109 imim2d
111 110 ralimdva
112 111 reximdva
113 50 112 syld
114 113 impr
115 45 46 114 mptnn0fsupp
116 3 15 21 27 29 35 44 115 gsummptmhm
117 simpll ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in \left({{K}}^{{ℕ}_{0}}\right)\wedge {finSupp}_{{0}_{{A}}}\left({M}\right)\right)\right)\wedge {n}\in {ℕ}_{0}\right)\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)$
118 1 2 3 4 5 6 7 8 9 10 11 12 13 14 monmat2matmon
119 117 41 42 118 syl12anc
120 119 mpteq2dva
121 120 oveq2d
122 116 121 eqtr3d