# Metamath Proof Explorer

## Theorem monmat2matmon

Description: The transformation of a polynomial matrix having scaled monomials with the same power as entries into a scaled monomial as a polynomial over matrices. (Contributed by AV, 11-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 monmat2matmon

### 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 crngring ${⊢}{R}\in \mathrm{CRing}\to {R}\in \mathrm{Ring}$
16 simpll ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\right)\right)\to {N}\in \mathrm{Fin}$
17 simplr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\right)\right)\to {R}\in \mathrm{Ring}$
18 7 8 14 1 2 3 13 11 12 mat2pmatscmxcl
19 1 2 3 4 5 6 7 9 10 pm2mpfval
20 16 17 18 19 syl3anc
21 15 20 sylanl2
22 simpll ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)$
23 simpr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\right)\right)\to \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\right)$
24 23 anim1i ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to \left(\left({M}\in {K}\wedge {L}\in {ℕ}_{0}\right)\wedge {k}\in {ℕ}_{0}\right)$
25 df-3an ${⊢}\left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {k}\in {ℕ}_{0}\right)↔\left(\left({M}\in {K}\wedge {L}\in {ℕ}_{0}\right)\wedge {k}\in {ℕ}_{0}\right)$
26 24 25 sylibr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\wedge {k}\in {ℕ}_{0}\right)$
27 eqid ${⊢}{0}_{{A}}={0}_{{A}}$
28 1 2 7 8 27 11 12 13 14 monmatcollpw
29 22 26 28 syl2anc
30 29 oveq1d
31 15 a1i ${⊢}{k}\in {ℕ}_{0}\to \left({R}\in \mathrm{CRing}\to {R}\in \mathrm{Ring}\right)$
32 31 anim2d ${⊢}{k}\in {ℕ}_{0}\to \left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\to \left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\right)$
33 32 anim1d ${⊢}{k}\in {ℕ}_{0}\to \left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\right)\right)\to \left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\right)\right)\right)$
34 33 imdistanri ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{CRing}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to \left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\right)\right)\wedge {k}\in {ℕ}_{0}\right)$
35 ovif
36 7 matring ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {A}\in \mathrm{Ring}$
37 9 ply1sca ${⊢}{A}\in \mathrm{Ring}\to {A}=\mathrm{Scalar}\left({Q}\right)$
38 36 37 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {A}=\mathrm{Scalar}\left({Q}\right)$
39 38 ad2antrr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to {A}=\mathrm{Scalar}\left({Q}\right)$
40 39 fveq2d ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to {0}_{{A}}={0}_{\mathrm{Scalar}\left({Q}\right)}$
41 40 oveq1d
42 9 ply1lmod ${⊢}{A}\in \mathrm{Ring}\to {Q}\in \mathrm{LMod}$
43 36 42 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {Q}\in \mathrm{LMod}$
44 43 ad2antrr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to {Q}\in \mathrm{LMod}$
45 9 ply1ring ${⊢}{A}\in \mathrm{Ring}\to {Q}\in \mathrm{Ring}$
46 36 45 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {Q}\in \mathrm{Ring}$
47 eqid ${⊢}{\mathrm{mulGrp}}_{{Q}}={\mathrm{mulGrp}}_{{Q}}$
48 47 ringmgp ${⊢}{Q}\in \mathrm{Ring}\to {\mathrm{mulGrp}}_{{Q}}\in \mathrm{Mnd}$
49 46 48 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {\mathrm{mulGrp}}_{{Q}}\in \mathrm{Mnd}$
50 49 ad2antrr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to {\mathrm{mulGrp}}_{{Q}}\in \mathrm{Mnd}$
51 simpr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to {k}\in {ℕ}_{0}$
52 eqid ${⊢}{\mathrm{Base}}_{{Q}}={\mathrm{Base}}_{{Q}}$
53 6 9 52 vr1cl ${⊢}{A}\in \mathrm{Ring}\to {X}\in {\mathrm{Base}}_{{Q}}$
54 36 53 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {X}\in {\mathrm{Base}}_{{Q}}$
55 54 ad2antrr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to {X}\in {\mathrm{Base}}_{{Q}}$
56 47 52 mgpbas ${⊢}{\mathrm{Base}}_{{Q}}={\mathrm{Base}}_{{\mathrm{mulGrp}}_{{Q}}}$
57 56 5 mulgnn0cl
58 50 51 55 57 syl3anc
59 eqid ${⊢}\mathrm{Scalar}\left({Q}\right)=\mathrm{Scalar}\left({Q}\right)$
60 eqid ${⊢}{0}_{\mathrm{Scalar}\left({Q}\right)}={0}_{\mathrm{Scalar}\left({Q}\right)}$
61 eqid ${⊢}{0}_{{Q}}={0}_{{Q}}$
62 52 59 4 60 61 lmod0vs
63 44 58 62 syl2anc
64 41 63 eqtrd
65 64 ifeq2d
66 35 65 syl5eq
67 34 66 syl
68 30 67 eqtrd
69 68 mpteq2dva
70 69 oveq2d
71 ringmnd ${⊢}{Q}\in \mathrm{Ring}\to {Q}\in \mathrm{Mnd}$
72 46 71 syl ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {Q}\in \mathrm{Mnd}$
73 72 adantr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\right)\right)\to {Q}\in \mathrm{Mnd}$
74 nn0ex ${⊢}{ℕ}_{0}\in \mathrm{V}$
75 74 a1i ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\right)\right)\to {ℕ}_{0}\in \mathrm{V}$
76 simprr ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\right)\right)\to {L}\in {ℕ}_{0}$
77 eqid
78 38 fveq2d ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {\mathrm{Base}}_{{A}}={\mathrm{Base}}_{\mathrm{Scalar}\left({Q}\right)}$
79 8 78 syl5eq ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {K}={\mathrm{Base}}_{\mathrm{Scalar}\left({Q}\right)}$
80 79 eleq2d ${⊢}\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to \left({M}\in {K}↔{M}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({Q}\right)}\right)$
81 80 biimpcd ${⊢}{M}\in {K}\to \left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {M}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({Q}\right)}\right)$
82 81 adantr ${⊢}\left({M}\in {K}\wedge {L}\in {ℕ}_{0}\right)\to \left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\to {M}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({Q}\right)}\right)$
83 82 impcom ${⊢}\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\right)\right)\to {M}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({Q}\right)}$
84 83 adantr ${⊢}\left(\left(\left({N}\in \mathrm{Fin}\wedge {R}\in \mathrm{Ring}\right)\wedge \left({M}\in {K}\wedge {L}\in {ℕ}_{0}\right)\right)\wedge {k}\in {ℕ}_{0}\right)\to {M}\in {\mathrm{Base}}_{\mathrm{Scalar}\left({Q}\right)}$
85 eqid ${⊢}{\mathrm{Base}}_{\mathrm{Scalar}\left({Q}\right)}={\mathrm{Base}}_{\mathrm{Scalar}\left({Q}\right)}$
86 52 59 4 85 lmodvscl
87 44 84 58 86 syl3anc
88 87 ralrimiva
89 61 73 75 76 77 88 gsummpt1n0
90 15 89 sylanl2
91 70 90 eqtrd
92 csbov2g
93 csbov1g
94 csbvarg
95 94 oveq1d
96 93 95 eqtrd
97 96 oveq2d
98 92 97 eqtrd