Metamath Proof Explorer


Theorem pmatcollpw3lem

Description: Lemma for pmatcollpw3 and pmatcollpw3fi : Write a polynomial matrix (over a commutative ring) as a sum of products of variable powers and constant matrices with scalar entries. (Contributed by AV, 8-Dec-2019)

Ref Expression
Hypotheses pmatcollpw.p P = Poly 1 R
pmatcollpw.c C = N Mat P
pmatcollpw.b B = Base C
pmatcollpw.m ˙ = C
pmatcollpw.e × ˙ = mulGrp P
pmatcollpw.x X = var 1 R
pmatcollpw.t T = N matToPolyMat R
pmatcollpw3.a A = N Mat R
pmatcollpw3.d D = Base A
Assertion pmatcollpw3lem N Fin R CRing M B I 0 I M = C n I n × ˙ X ˙ T M decompPMat n f D I M = C n I n × ˙ X ˙ T f n

Proof

Step Hyp Ref Expression
1 pmatcollpw.p P = Poly 1 R
2 pmatcollpw.c C = N Mat P
3 pmatcollpw.b B = Base C
4 pmatcollpw.m ˙ = C
5 pmatcollpw.e × ˙ = mulGrp P
6 pmatcollpw.x X = var 1 R
7 pmatcollpw.t T = N matToPolyMat R
8 pmatcollpw3.a A = N Mat R
9 pmatcollpw3.d D = Base A
10 dmeq x = y dom x = dom y
11 10 dmeqd x = y dom dom x = dom dom y
12 oveq x = y i x j = i y j
13 12 fveq2d x = y coe 1 i x j = coe 1 i y j
14 13 fveq1d x = y coe 1 i x j k = coe 1 i y j k
15 11 11 14 mpoeq123dv x = y i dom dom x , j dom dom x coe 1 i x j k = i dom dom y , j dom dom y coe 1 i y j k
16 fveq2 k = l coe 1 i y j k = coe 1 i y j l
17 16 mpoeq3dv k = l i dom dom y , j dom dom y coe 1 i y j k = i dom dom y , j dom dom y coe 1 i y j l
18 15 17 cbvmpov x B , k I i dom dom x , j dom dom x coe 1 i x j k = y B , l I i dom dom y , j dom dom y coe 1 i y j l
19 dmexg y B dom y V
20 19 dmexd y B dom dom y V
21 20 20 jca y B dom dom y V dom dom y V
22 21 ad2antrl N Fin R CRing M B I 0 I y B l I dom dom y V dom dom y V
23 mpoexga dom dom y V dom dom y V i dom dom y , j dom dom y coe 1 i y j l V
24 22 23 syl N Fin R CRing M B I 0 I y B l I i dom dom y , j dom dom y coe 1 i y j l V
25 24 ralrimivva N Fin R CRing M B I 0 I y B l I i dom dom y , j dom dom y coe 1 i y j l V
26 simprr N Fin R CRing M B I 0 I I
27 nn0ex 0 V
28 27 ssex I 0 I V
29 28 ad2antrl N Fin R CRing M B I 0 I I V
30 simp3 N Fin R CRing M B M B
31 30 adantr N Fin R CRing M B I 0 I M B
32 18 25 26 29 31 mpocurryvald N Fin R CRing M B I 0 I curry x B , k I i dom dom x , j dom dom x coe 1 i x j k M = l I M / y i dom dom y , j dom dom y coe 1 i y j l
33 fveq2 l = k coe 1 i y j l = coe 1 i y j k
34 33 mpoeq3dv l = k i dom dom y , j dom dom y coe 1 i y j l = i dom dom y , j dom dom y coe 1 i y j k
35 34 csbeq2dv l = k M / y i dom dom y , j dom dom y coe 1 i y j l = M / y i dom dom y , j dom dom y coe 1 i y j k
36 eqcom x = y y = x
37 eqcom i dom dom x , j dom dom x coe 1 i x j k = i dom dom y , j dom dom y coe 1 i y j k i dom dom y , j dom dom y coe 1 i y j k = i dom dom x , j dom dom x coe 1 i x j k
38 15 36 37 3imtr3i y = x i dom dom y , j dom dom y coe 1 i y j k = i dom dom x , j dom dom x coe 1 i x j k
39 38 cbvcsbv M / y i dom dom y , j dom dom y coe 1 i y j k = M / x i dom dom x , j dom dom x coe 1 i x j k
40 35 39 eqtrdi l = k M / y i dom dom y , j dom dom y coe 1 i y j l = M / x i dom dom x , j dom dom x coe 1 i x j k
41 40 cbvmptv l I M / y i dom dom y , j dom dom y coe 1 i y j l = k I M / x i dom dom x , j dom dom x coe 1 i x j k
42 32 41 eqtrdi N Fin R CRing M B I 0 I curry x B , k I i dom dom x , j dom dom x coe 1 i x j k M = k I M / x i dom dom x , j dom dom x coe 1 i x j k
43 dmeq x = M dom x = dom M
44 43 dmeqd x = M dom dom x = dom dom M
45 oveq x = M i x j = i M j
46 45 fveq2d x = M coe 1 i x j = coe 1 i M j
47 46 fveq1d x = M coe 1 i x j k = coe 1 i M j k
48 44 44 47 mpoeq123dv x = M i dom dom x , j dom dom x coe 1 i x j k = i dom dom M , j dom dom M coe 1 i M j k
49 48 adantl N Fin R CRing M B x = M i dom dom x , j dom dom x coe 1 i x j k = i dom dom M , j dom dom M coe 1 i M j k
50 30 49 csbied N Fin R CRing M B M / x i dom dom x , j dom dom x coe 1 i x j k = i dom dom M , j dom dom M coe 1 i M j k
51 eqid Base P = Base P
52 2 51 3 matbas2i M B M Base P N × N
53 elmapi M Base P N × N M : N × N Base P
54 fdm M : N × N Base P dom M = N × N
55 54 dmeqd M : N × N Base P dom dom M = dom N × N
56 dmxpid dom N × N = N
57 55 56 eqtr2di M : N × N Base P N = dom dom M
58 52 53 57 3syl M B N = dom dom M
59 58 3ad2ant3 N Fin R CRing M B N = dom dom M
60 59 adantr N Fin R CRing M B m = M N = dom dom M
61 simpr N Fin R CRing M B m = M m = M
62 61 oveqd N Fin R CRing M B m = M i m j = i M j
63 62 fveq2d N Fin R CRing M B m = M coe 1 i m j = coe 1 i M j
64 63 fveq1d N Fin R CRing M B m = M coe 1 i m j k = coe 1 i M j k
65 60 60 64 mpoeq123dv N Fin R CRing M B m = M i N , j N coe 1 i m j k = i dom dom M , j dom dom M coe 1 i M j k
66 30 65 csbied N Fin R CRing M B M / m i N , j N coe 1 i m j k = i dom dom M , j dom dom M coe 1 i M j k
67 50 66 eqtr4d N Fin R CRing M B M / x i dom dom x , j dom dom x coe 1 i x j k = M / m i N , j N coe 1 i m j k
68 67 adantr N Fin R CRing M B I 0 I M / x i dom dom x , j dom dom x coe 1 i x j k = M / m i N , j N coe 1 i m j k
69 68 mpteq2dv N Fin R CRing M B I 0 I k I M / x i dom dom x , j dom dom x coe 1 i x j k = k I M / m i N , j N coe 1 i m j k
70 42 69 eqtrd N Fin R CRing M B I 0 I curry x B , k I i dom dom x , j dom dom x coe 1 i x j k M = k I M / m i N , j N coe 1 i m j k
71 oveq m = M i m j = i M j
72 71 adantl N Fin R CRing M B m = M i m j = i M j
73 72 fveq2d N Fin R CRing M B m = M coe 1 i m j = coe 1 i M j
74 73 fveq1d N Fin R CRing M B m = M coe 1 i m j k = coe 1 i M j k
75 74 mpoeq3dv N Fin R CRing M B m = M i N , j N coe 1 i m j k = i N , j N coe 1 i M j k
76 30 75 csbied N Fin R CRing M B M / m i N , j N coe 1 i m j k = i N , j N coe 1 i M j k
77 76 ad2antrr N Fin R CRing M B I 0 I k I M / m i N , j N coe 1 i m j k = i N , j N coe 1 i M j k
78 eqid Base R = Base R
79 simpll1 N Fin R CRing M B I 0 I k I N Fin
80 simpll2 N Fin R CRing M B I 0 I k I R CRing
81 simp2 N Fin R CRing M B I 0 I k I i N j N i N
82 simp3 N Fin R CRing M B I 0 I k I i N j N j N
83 31 adantr N Fin R CRing M B I 0 I k I M B
84 83 3ad2ant1 N Fin R CRing M B I 0 I k I i N j N M B
85 2 51 3 81 82 84 matecld N Fin R CRing M B I 0 I k I i N j N i M j Base P
86 ssel I 0 k I k 0
87 86 ad2antrl N Fin R CRing M B I 0 I k I k 0
88 87 imp N Fin R CRing M B I 0 I k I k 0
89 88 3ad2ant1 N Fin R CRing M B I 0 I k I i N j N k 0
90 eqid coe 1 i M j = coe 1 i M j
91 90 51 1 78 coe1fvalcl i M j Base P k 0 coe 1 i M j k Base R
92 85 89 91 syl2anc N Fin R CRing M B I 0 I k I i N j N coe 1 i M j k Base R
93 8 78 9 79 80 92 matbas2d N Fin R CRing M B I 0 I k I i N , j N coe 1 i M j k D
94 77 93 eqeltrd N Fin R CRing M B I 0 I k I M / m i N , j N coe 1 i m j k D
95 94 fmpttd N Fin R CRing M B I 0 I k I M / m i N , j N coe 1 i m j k : I D
96 9 fvexi D V
97 96 a1i N Fin R CRing M B D V
98 28 adantr I 0 I I V
99 elmapg D V I V k I M / m i N , j N coe 1 i m j k D I k I M / m i N , j N coe 1 i m j k : I D
100 97 98 99 syl2an N Fin R CRing M B I 0 I k I M / m i N , j N coe 1 i m j k D I k I M / m i N , j N coe 1 i m j k : I D
101 95 100 mpbird N Fin R CRing M B I 0 I k I M / m i N , j N coe 1 i m j k D I
102 70 101 eqeltrd N Fin R CRing M B I 0 I curry x B , k I i dom dom x , j dom dom x coe 1 i x j k M D I
103 fveq1 f = curry x B , k I i dom dom x , j dom dom x coe 1 i x j k M f n = curry x B , k I i dom dom x , j dom dom x coe 1 i x j k M n
104 103 adantl N Fin R CRing M B I 0 I f = curry x B , k I i dom dom x , j dom dom x coe 1 i x j k M f n = curry x B , k I i dom dom x , j dom dom x coe 1 i x j k M n
105 104 adantr N Fin R CRing M B I 0 I f = curry x B , k I i dom dom x , j dom dom x coe 1 i x j k M n I f n = curry x B , k I i dom dom x , j dom dom x coe 1 i x j k M n
106 eqid x B , k I i dom dom x , j dom dom x coe 1 i x j k = x B , k I i dom dom x , j dom dom x coe 1 i x j k
107 dmexg x B dom x V
108 107 dmexd x B dom dom x V
109 108 108 jca x B dom dom x V dom dom x V
110 109 ad2antrl N Fin R CRing M B I 0 I n I x B k I dom dom x V dom dom x V
111 mpoexga dom dom x V dom dom x V i dom dom x , j dom dom x coe 1 i x j k V
112 110 111 syl N Fin R CRing M B I 0 I n I x B k I i dom dom x , j dom dom x coe 1 i x j k V
113 112 ralrimivva N Fin R CRing M B I 0 I n I x B k I i dom dom x , j dom dom x coe 1 i x j k V
114 29 adantr N Fin R CRing M B I 0 I n I I V
115 31 adantr N Fin R CRing M B I 0 I n I M B
116 simpr N Fin R CRing M B I 0 I n I n I
117 106 113 114 115 116 fvmpocurryd N Fin R CRing M B I 0 I n I curry x B , k I i dom dom x , j dom dom x coe 1 i x j k M n = M x B , k I i dom dom x , j dom dom x coe 1 i x j k n
118 df-decpmat decompPMat = x V , k 0 i dom dom x , j dom dom x coe 1 i x j k
119 118 reseq1i decompPMat B × I = x V , k 0 i dom dom x , j dom dom x coe 1 i x j k B × I
120 ssv B V
121 120 a1i N Fin R CRing M B B V
122 simpl I 0 I I 0
123 121 122 anim12i N Fin R CRing M B I 0 I B V I 0
124 123 adantr N Fin R CRing M B I 0 I n I B V I 0
125 resmpo B V I 0 x V , k 0 i dom dom x , j dom dom x coe 1 i x j k B × I = x B , k I i dom dom x , j dom dom x coe 1 i x j k
126 124 125 syl N Fin R CRing M B I 0 I n I x V , k 0 i dom dom x , j dom dom x coe 1 i x j k B × I = x B , k I i dom dom x , j dom dom x coe 1 i x j k
127 119 126 eqtr2id N Fin R CRing M B I 0 I n I x B , k I i dom dom x , j dom dom x coe 1 i x j k = decompPMat B × I
128 127 oveqd N Fin R CRing M B I 0 I n I M x B , k I i dom dom x , j dom dom x coe 1 i x j k n = M decompPMat B × I n
129 117 128 eqtrd N Fin R CRing M B I 0 I n I curry x B , k I i dom dom x , j dom dom x coe 1 i x j k M n = M decompPMat B × I n
130 129 adantlr N Fin R CRing M B I 0 I f = curry x B , k I i dom dom x , j dom dom x coe 1 i x j k M n I curry x B , k I i dom dom x , j dom dom x coe 1 i x j k M n = M decompPMat B × I n
131 105 130 eqtrd N Fin R CRing M B I 0 I f = curry x B , k I i dom dom x , j dom dom x coe 1 i x j k M n I f n = M decompPMat B × I n
132 131 fveq2d N Fin R CRing M B I 0 I f = curry x B , k I i dom dom x , j dom dom x coe 1 i x j k M n I T f n = T M decompPMat B × I n
133 30 ad2antrr N Fin R CRing M B I 0 I f = curry x B , k I i dom dom x , j dom dom x coe 1 i x j k M M B
134 ovres M B n I M decompPMat B × I n = M decompPMat n
135 133 134 sylan N Fin R CRing M B I 0 I f = curry x B , k I i dom dom x , j dom dom x coe 1 i x j k M n I M decompPMat B × I n = M decompPMat n
136 135 fveq2d N Fin R CRing M B I 0 I f = curry x B , k I i dom dom x , j dom dom x coe 1 i x j k M n I T M decompPMat B × I n = T M decompPMat n
137 132 136 eqtrd N Fin R CRing M B I 0 I f = curry x B , k I i dom dom x , j dom dom x coe 1 i x j k M n I T f n = T M decompPMat n
138 137 oveq2d N Fin R CRing M B I 0 I f = curry x B , k I i dom dom x , j dom dom x coe 1 i x j k M n I n × ˙ X ˙ T f n = n × ˙ X ˙ T M decompPMat n
139 138 mpteq2dva N Fin R CRing M B I 0 I f = curry x B , k I i dom dom x , j dom dom x coe 1 i x j k M n I n × ˙ X ˙ T f n = n I n × ˙ X ˙ T M decompPMat n
140 139 oveq2d N Fin R CRing M B I 0 I f = curry x B , k I i dom dom x , j dom dom x coe 1 i x j k M C n I n × ˙ X ˙ T f n = C n I n × ˙ X ˙ T M decompPMat n
141 140 eqeq2d N Fin R CRing M B I 0 I f = curry x B , k I i dom dom x , j dom dom x coe 1 i x j k M M = C n I n × ˙ X ˙ T f n M = C n I n × ˙ X ˙ T M decompPMat n
142 102 141 rspcedv N Fin R CRing M B I 0 I M = C n I n × ˙ X ˙ T M decompPMat n f D I M = C n I n × ˙ X ˙ T f n