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 = Poly 1 R
monmat2matmon.c C = N Mat P
monmat2matmon.b B = Base C
monmat2matmon.m1 ˙ = Q
monmat2matmon.e1 × ˙ = mulGrp Q
monmat2matmon.x X = var 1 A
monmat2matmon.a A = N Mat R
monmat2matmon.k K = Base A
monmat2matmon.q Q = Poly 1 A
monmat2matmon.i I = N pMatToMatPoly R
monmat2matmon.e2 E = mulGrp P
monmat2matmon.y Y = var 1 R
monmat2matmon.m2 · ˙ = C
monmat2matmon.t T = N matToPolyMat R
Assertion monmat2matmon N Fin R CRing M K L 0 I L E Y · ˙ T M = M ˙ L × ˙ X

Proof

Step Hyp Ref Expression
1 monmat2matmon.p P = Poly 1 R
2 monmat2matmon.c C = N Mat P
3 monmat2matmon.b B = Base C
4 monmat2matmon.m1 ˙ = Q
5 monmat2matmon.e1 × ˙ = mulGrp Q
6 monmat2matmon.x X = var 1 A
7 monmat2matmon.a A = N Mat R
8 monmat2matmon.k K = Base A
9 monmat2matmon.q Q = Poly 1 A
10 monmat2matmon.i I = N pMatToMatPoly R
11 monmat2matmon.e2 E = mulGrp P
12 monmat2matmon.y Y = var 1 R
13 monmat2matmon.m2 · ˙ = C
14 monmat2matmon.t T = N matToPolyMat R
15 crngring R CRing R Ring
16 simpll N Fin R Ring M K L 0 N Fin
17 simplr N Fin R Ring M K L 0 R Ring
18 7 8 14 1 2 3 13 11 12 mat2pmatscmxcl N Fin R Ring M K L 0 L E Y · ˙ T M B
19 1 2 3 4 5 6 7 9 10 pm2mpfval N Fin R Ring L E Y · ˙ T M B I L E Y · ˙ T M = Q k 0 L E Y · ˙ T M decompPMat k ˙ k × ˙ X
20 16 17 18 19 syl3anc N Fin R Ring M K L 0 I L E Y · ˙ T M = Q k 0 L E Y · ˙ T M decompPMat k ˙ k × ˙ X
21 15 20 sylanl2 N Fin R CRing M K L 0 I L E Y · ˙ T M = Q k 0 L E Y · ˙ T M decompPMat k ˙ k × ˙ X
22 simpll N Fin R CRing M K L 0 k 0 N Fin R CRing
23 simpr N Fin R CRing M K L 0 M K L 0
24 23 anim1i N Fin R CRing M K L 0 k 0 M K L 0 k 0
25 df-3an M K L 0 k 0 M K L 0 k 0
26 24 25 sylibr N Fin R CRing M K L 0 k 0 M K L 0 k 0
27 eqid 0 A = 0 A
28 1 2 7 8 27 11 12 13 14 monmatcollpw N Fin R CRing M K L 0 k 0 L E Y · ˙ T M decompPMat k = if k = L M 0 A
29 22 26 28 syl2anc N Fin R CRing M K L 0 k 0 L E Y · ˙ T M decompPMat k = if k = L M 0 A
30 29 oveq1d N Fin R CRing M K L 0 k 0 L E Y · ˙ T M decompPMat k ˙ k × ˙ X = if k = L M 0 A ˙ k × ˙ X
31 15 a1i k 0 R CRing R Ring
32 31 anim2d k 0 N Fin R CRing N Fin R Ring
33 32 anim1d k 0 N Fin R CRing M K L 0 N Fin R Ring M K L 0
34 33 imdistanri N Fin R CRing M K L 0 k 0 N Fin R Ring M K L 0 k 0
35 ovif if k = L M 0 A ˙ k × ˙ X = if k = L M ˙ k × ˙ X 0 A ˙ k × ˙ X
36 7 matring N Fin R Ring A Ring
37 9 ply1sca A Ring A = Scalar Q
38 36 37 syl N Fin R Ring A = Scalar Q
39 38 ad2antrr N Fin R Ring M K L 0 k 0 A = Scalar Q
40 39 fveq2d N Fin R Ring M K L 0 k 0 0 A = 0 Scalar Q
41 40 oveq1d N Fin R Ring M K L 0 k 0 0 A ˙ k × ˙ X = 0 Scalar Q ˙ k × ˙ X
42 9 ply1lmod A Ring Q LMod
43 36 42 syl N Fin R Ring Q LMod
44 43 ad2antrr N Fin R Ring M K L 0 k 0 Q LMod
45 9 ply1ring A Ring Q Ring
46 36 45 syl N Fin R Ring Q Ring
47 eqid mulGrp Q = mulGrp Q
48 47 ringmgp Q Ring mulGrp Q Mnd
49 46 48 syl N Fin R Ring mulGrp Q Mnd
50 49 ad2antrr N Fin R Ring M K L 0 k 0 mulGrp Q Mnd
51 simpr N Fin R Ring M K L 0 k 0 k 0
52 eqid Base Q = Base Q
53 6 9 52 vr1cl A Ring X Base Q
54 36 53 syl N Fin R Ring X Base Q
55 54 ad2antrr N Fin R Ring M K L 0 k 0 X Base Q
56 47 52 mgpbas Base Q = Base mulGrp Q
57 56 5 mulgnn0cl mulGrp Q Mnd k 0 X Base Q k × ˙ X Base Q
58 50 51 55 57 syl3anc N Fin R Ring M K L 0 k 0 k × ˙ X Base Q
59 eqid Scalar Q = Scalar Q
60 eqid 0 Scalar Q = 0 Scalar Q
61 eqid 0 Q = 0 Q
62 52 59 4 60 61 lmod0vs Q LMod k × ˙ X Base Q 0 Scalar Q ˙ k × ˙ X = 0 Q
63 44 58 62 syl2anc N Fin R Ring M K L 0 k 0 0 Scalar Q ˙ k × ˙ X = 0 Q
64 41 63 eqtrd N Fin R Ring M K L 0 k 0 0 A ˙ k × ˙ X = 0 Q
65 64 ifeq2d N Fin R Ring M K L 0 k 0 if k = L M ˙ k × ˙ X 0 A ˙ k × ˙ X = if k = L M ˙ k × ˙ X 0 Q
66 35 65 eqtrid N Fin R Ring M K L 0 k 0 if k = L M 0 A ˙ k × ˙ X = if k = L M ˙ k × ˙ X 0 Q
67 34 66 syl N Fin R CRing M K L 0 k 0 if k = L M 0 A ˙ k × ˙ X = if k = L M ˙ k × ˙ X 0 Q
68 30 67 eqtrd N Fin R CRing M K L 0 k 0 L E Y · ˙ T M decompPMat k ˙ k × ˙ X = if k = L M ˙ k × ˙ X 0 Q
69 68 mpteq2dva N Fin R CRing M K L 0 k 0 L E Y · ˙ T M decompPMat k ˙ k × ˙ X = k 0 if k = L M ˙ k × ˙ X 0 Q
70 69 oveq2d N Fin R CRing M K L 0 Q k 0 L E Y · ˙ T M decompPMat k ˙ k × ˙ X = Q k 0 if k = L M ˙ k × ˙ X 0 Q
71 ringmnd Q Ring Q Mnd
72 46 71 syl N Fin R Ring Q Mnd
73 72 adantr N Fin R Ring M K L 0 Q Mnd
74 nn0ex 0 V
75 74 a1i N Fin R Ring M K L 0 0 V
76 simprr N Fin R Ring M K L 0 L 0
77 eqid k 0 if k = L M ˙ k × ˙ X 0 Q = k 0 if k = L M ˙ k × ˙ X 0 Q
78 38 fveq2d N Fin R Ring Base A = Base Scalar Q
79 8 78 eqtrid N Fin R Ring K = Base Scalar Q
80 79 eleq2d N Fin R Ring M K M Base Scalar Q
81 80 biimpcd M K N Fin R Ring M Base Scalar Q
82 81 adantr M K L 0 N Fin R Ring M Base Scalar Q
83 82 impcom N Fin R Ring M K L 0 M Base Scalar Q
84 83 adantr N Fin R Ring M K L 0 k 0 M Base Scalar Q
85 eqid Base Scalar Q = Base Scalar Q
86 52 59 4 85 lmodvscl Q LMod M Base Scalar Q k × ˙ X Base Q M ˙ k × ˙ X Base Q
87 44 84 58 86 syl3anc N Fin R Ring M K L 0 k 0 M ˙ k × ˙ X Base Q
88 87 ralrimiva N Fin R Ring M K L 0 k 0 M ˙ k × ˙ X Base Q
89 61 73 75 76 77 88 gsummpt1n0 N Fin R Ring M K L 0 Q k 0 if k = L M ˙ k × ˙ X 0 Q = L / k M ˙ k × ˙ X
90 15 89 sylanl2 N Fin R CRing M K L 0 Q k 0 if k = L M ˙ k × ˙ X 0 Q = L / k M ˙ k × ˙ X
91 70 90 eqtrd N Fin R CRing M K L 0 Q k 0 L E Y · ˙ T M decompPMat k ˙ k × ˙ X = L / k M ˙ k × ˙ X
92 csbov2g L 0 L / k M ˙ k × ˙ X = M ˙ L / k k × ˙ X
93 csbov1g L 0 L / k k × ˙ X = L / k k × ˙ X
94 csbvarg L 0 L / k k = L
95 94 oveq1d L 0 L / k k × ˙ X = L × ˙ X
96 93 95 eqtrd L 0 L / k k × ˙ X = L × ˙ X
97 96 oveq2d L 0 M ˙ L / k k × ˙ X = M ˙ L × ˙ X
98 92 97 eqtrd L 0 L / k M ˙ k × ˙ X = M ˙ L × ˙ X
99 98 ad2antll N Fin R CRing M K L 0 L / k M ˙ k × ˙ X = M ˙ L × ˙ X
100 21 91 99 3eqtrd N Fin R CRing M K L 0 I L E Y · ˙ T M = M ˙ L × ˙ X