Metamath Proof Explorer


Theorem cpmadugsumlemF

Description: Lemma F for cpmadugsum . (Contributed by AV, 7-Nov-2019)

Ref Expression
Hypotheses cpmadugsum.a A = N Mat R
cpmadugsum.b B = Base A
cpmadugsum.p P = Poly 1 R
cpmadugsum.y Y = N Mat P
cpmadugsum.t T = N matToPolyMat R
cpmadugsum.x X = var 1 R
cpmadugsum.e × ˙ = mulGrp P
cpmadugsum.m · ˙ = Y
cpmadugsum.r × ˙ = Y
cpmadugsum.1 1 ˙ = 1 Y
cpmadugsum.g + ˙ = + Y
cpmadugsum.s - ˙ = - Y
Assertion cpmadugsumlemF N Fin R CRing M B s b B 0 s X · ˙ 1 ˙ × ˙ Y i = 0 s i × ˙ X · ˙ T b i - ˙ T M × ˙ Y i = 0 s i × ˙ X · ˙ T b i = Y i = 1 s i × ˙ X · ˙ T b i 1 - ˙ T M × ˙ T b i + ˙ s + 1 × ˙ X · ˙ T b s - ˙ T M × ˙ T b 0

Proof

Step Hyp Ref Expression
1 cpmadugsum.a A = N Mat R
2 cpmadugsum.b B = Base A
3 cpmadugsum.p P = Poly 1 R
4 cpmadugsum.y Y = N Mat P
5 cpmadugsum.t T = N matToPolyMat R
6 cpmadugsum.x X = var 1 R
7 cpmadugsum.e × ˙ = mulGrp P
8 cpmadugsum.m · ˙ = Y
9 cpmadugsum.r × ˙ = Y
10 cpmadugsum.1 1 ˙ = 1 Y
11 cpmadugsum.g + ˙ = + Y
12 cpmadugsum.s - ˙ = - Y
13 nnnn0 s s 0
14 1 2 3 4 5 6 7 8 9 10 cpmadugsumlemB N Fin R CRing M B s 0 b B 0 s X · ˙ 1 ˙ × ˙ Y i = 0 s i × ˙ X · ˙ T b i = Y i = 0 s i + 1 × ˙ X · ˙ T b i
15 13 14 sylanr1 N Fin R CRing M B s b B 0 s X · ˙ 1 ˙ × ˙ Y i = 0 s i × ˙ X · ˙ T b i = Y i = 0 s i + 1 × ˙ X · ˙ T b i
16 1 2 3 4 5 6 7 8 9 10 cpmadugsumlemC N Fin R CRing M B s 0 b B 0 s T M × ˙ Y i = 0 s i × ˙ X · ˙ T b i = Y i = 0 s i × ˙ X · ˙ T M × ˙ T b i
17 13 16 sylanr1 N Fin R CRing M B s b B 0 s T M × ˙ Y i = 0 s i × ˙ X · ˙ T b i = Y i = 0 s i × ˙ X · ˙ T M × ˙ T b i
18 15 17 oveq12d N Fin R CRing M B s b B 0 s X · ˙ 1 ˙ × ˙ Y i = 0 s i × ˙ X · ˙ T b i - ˙ T M × ˙ Y i = 0 s i × ˙ X · ˙ T b i = Y i = 0 s i + 1 × ˙ X · ˙ T b i - ˙ Y i = 0 s i × ˙ X · ˙ T M × ˙ T b i
19 nncn s s
20 npcan1 s s - 1 + 1 = s
21 20 eqcomd s s = s - 1 + 1
22 19 21 syl s s = s - 1 + 1
23 22 oveq2d s 0 s = 0 s - 1 + 1
24 23 mpteq1d s i 0 s i + 1 × ˙ X · ˙ T b i = i 0 s - 1 + 1 i + 1 × ˙ X · ˙ T b i
25 24 oveq2d s Y i = 0 s i + 1 × ˙ X · ˙ T b i = Y i = 0 s - 1 + 1 i + 1 × ˙ X · ˙ T b i
26 25 ad2antrl N Fin R CRing M B s b B 0 s Y i = 0 s i + 1 × ˙ X · ˙ T b i = Y i = 0 s - 1 + 1 i + 1 × ˙ X · ˙ T b i
27 eqid Base Y = Base Y
28 crngring R CRing R Ring
29 28 anim2i N Fin R CRing N Fin R Ring
30 29 3adant3 N Fin R CRing M B N Fin R Ring
31 3 4 pmatring N Fin R Ring Y Ring
32 30 31 syl N Fin R CRing M B Y Ring
33 ringcmn Y Ring Y CMnd
34 32 33 syl N Fin R CRing M B Y CMnd
35 34 adantr N Fin R CRing M B s b B 0 s Y CMnd
36 nnm1nn0 s s 1 0
37 36 ad2antrl N Fin R CRing M B s b B 0 s s 1 0
38 simpll1 N Fin R CRing M B s b B 0 s i 0 s - 1 + 1 N Fin
39 28 3ad2ant2 N Fin R CRing M B R Ring
40 39 adantr N Fin R CRing M B s b B 0 s R Ring
41 40 adantr N Fin R CRing M B s b B 0 s i 0 s - 1 + 1 R Ring
42 elmapi b B 0 s b : 0 s B
43 23 feq2d s b : 0 s B b : 0 s - 1 + 1 B
44 42 43 syl5ibcom b B 0 s s b : 0 s - 1 + 1 B
45 44 impcom s b B 0 s b : 0 s - 1 + 1 B
46 45 adantl N Fin R CRing M B s b B 0 s b : 0 s - 1 + 1 B
47 46 ffvelcdmda N Fin R CRing M B s b B 0 s i 0 s - 1 + 1 b i B
48 elfznn0 i 0 s - 1 + 1 i 0
49 48 adantl N Fin R CRing M B s b B 0 s i 0 s - 1 + 1 i 0
50 1nn0 1 0
51 50 a1i N Fin R CRing M B s b B 0 s i 0 s - 1 + 1 1 0
52 49 51 nn0addcld N Fin R CRing M B s b B 0 s i 0 s - 1 + 1 i + 1 0
53 1 2 5 3 4 27 8 7 6 mat2pmatscmxcl N Fin R Ring b i B i + 1 0 i + 1 × ˙ X · ˙ T b i Base Y
54 38 41 47 52 53 syl22anc N Fin R CRing M B s b B 0 s i 0 s - 1 + 1 i + 1 × ˙ X · ˙ T b i Base Y
55 27 11 35 37 54 gsummptfzsplit N Fin R CRing M B s b B 0 s Y i = 0 s - 1 + 1 i + 1 × ˙ X · ˙ T b i = Y i = 0 s 1 i + 1 × ˙ X · ˙ T b i + ˙ Y i s - 1 + 1 i + 1 × ˙ X · ˙ T b i
56 ringmnd Y Ring Y Mnd
57 32 56 syl N Fin R CRing M B Y Mnd
58 57 adantr N Fin R CRing M B s b B 0 s Y Mnd
59 ovexd N Fin R CRing M B s b B 0 s s - 1 + 1 V
60 simpl1 N Fin R CRing M B s b B 0 s N Fin
61 nn0fz0 s 0 s 0 s
62 13 61 sylib s s 0 s
63 ffvelcdm b : 0 s B s 0 s b s B
64 42 62 63 syl2anr s b B 0 s b s B
65 13 adantr s b B 0 s s 0
66 50 a1i s b B 0 s 1 0
67 65 66 nn0addcld s b B 0 s s + 1 0
68 64 67 jca s b B 0 s b s B s + 1 0
69 68 adantl N Fin R CRing M B s b B 0 s b s B s + 1 0
70 1 2 5 3 4 27 8 7 6 mat2pmatscmxcl N Fin R Ring b s B s + 1 0 s + 1 × ˙ X · ˙ T b s Base Y
71 60 40 69 70 syl21anc N Fin R CRing M B s b B 0 s s + 1 × ˙ X · ˙ T b s Base Y
72 oveq1 i = s - 1 + 1 i + 1 = s 1 + 1 + 1
73 72 oveq1d i = s - 1 + 1 i + 1 × ˙ X = s 1 + 1 + 1 × ˙ X
74 2fveq3 i = s - 1 + 1 T b i = T b s - 1 + 1
75 73 74 oveq12d i = s - 1 + 1 i + 1 × ˙ X · ˙ T b i = s 1 + 1 + 1 × ˙ X · ˙ T b s - 1 + 1
76 19 20 syl s s - 1 + 1 = s
77 76 oveq1d s s 1 + 1 + 1 = s + 1
78 77 oveq1d s s 1 + 1 + 1 × ˙ X = s + 1 × ˙ X
79 76 fveq2d s b s - 1 + 1 = b s
80 79 fveq2d s T b s - 1 + 1 = T b s
81 78 80 oveq12d s s 1 + 1 + 1 × ˙ X · ˙ T b s - 1 + 1 = s + 1 × ˙ X · ˙ T b s
82 81 ad2antrl N Fin R CRing M B s b B 0 s s 1 + 1 + 1 × ˙ X · ˙ T b s - 1 + 1 = s + 1 × ˙ X · ˙ T b s
83 75 82 sylan9eqr N Fin R CRing M B s b B 0 s i = s - 1 + 1 i + 1 × ˙ X · ˙ T b i = s + 1 × ˙ X · ˙ T b s
84 27 58 59 71 83 gsumsnd N Fin R CRing M B s b B 0 s Y i s - 1 + 1 i + 1 × ˙ X · ˙ T b i = s + 1 × ˙ X · ˙ T b s
85 84 oveq2d N Fin R CRing M B s b B 0 s Y i = 0 s 1 i + 1 × ˙ X · ˙ T b i + ˙ Y i s - 1 + 1 i + 1 × ˙ X · ˙ T b i = Y i = 0 s 1 i + 1 × ˙ X · ˙ T b i + ˙ s + 1 × ˙ X · ˙ T b s
86 26 55 85 3eqtrd N Fin R CRing M B s b B 0 s Y i = 0 s i + 1 × ˙ X · ˙ T b i = Y i = 0 s 1 i + 1 × ˙ X · ˙ T b i + ˙ s + 1 × ˙ X · ˙ T b s
87 13 ad2antrl N Fin R CRing M B s b B 0 s s 0
88 3 4 pmatlmod N Fin R Ring Y LMod
89 29 88 syl N Fin R CRing Y LMod
90 89 3adant3 N Fin R CRing M B Y LMod
91 90 adantr N Fin R CRing M B s b B 0 s Y LMod
92 91 adantr N Fin R CRing M B s b B 0 s i 0 s Y LMod
93 eqid mulGrp P = mulGrp P
94 eqid Base P = Base P
95 93 94 mgpbas Base P = Base mulGrp P
96 3 ply1ring R Ring P Ring
97 28 96 syl R CRing P Ring
98 97 3ad2ant2 N Fin R CRing M B P Ring
99 93 ringmgp P Ring mulGrp P Mnd
100 98 99 syl N Fin R CRing M B mulGrp P Mnd
101 100 adantr N Fin R CRing M B s b B 0 s mulGrp P Mnd
102 101 adantr N Fin R CRing M B s b B 0 s i 0 s mulGrp P Mnd
103 elfznn0 i 0 s i 0
104 103 adantl N Fin R CRing M B s b B 0 s i 0 s i 0
105 6 3 94 vr1cl R Ring X Base P
106 28 105 syl R CRing X Base P
107 106 3ad2ant2 N Fin R CRing M B X Base P
108 107 adantr N Fin R CRing M B s b B 0 s X Base P
109 108 adantr N Fin R CRing M B s b B 0 s i 0 s X Base P
110 95 7 102 104 109 mulgnn0cld N Fin R CRing M B s b B 0 s i 0 s i × ˙ X Base P
111 3 ply1crng R CRing P CRing
112 111 anim2i N Fin R CRing N Fin P CRing
113 112 3adant3 N Fin R CRing M B N Fin P CRing
114 4 matsca2 N Fin P CRing P = Scalar Y
115 113 114 syl N Fin R CRing M B P = Scalar Y
116 115 eqcomd N Fin R CRing M B Scalar Y = P
117 116 fveq2d N Fin R CRing M B Base Scalar Y = Base P
118 117 eleq2d N Fin R CRing M B i × ˙ X Base Scalar Y i × ˙ X Base P
119 118 adantr N Fin R CRing M B s b B 0 s i × ˙ X Base Scalar Y i × ˙ X Base P
120 119 adantr N Fin R CRing M B s b B 0 s i 0 s i × ˙ X Base Scalar Y i × ˙ X Base P
121 110 120 mpbird N Fin R CRing M B s b B 0 s i 0 s i × ˙ X Base Scalar Y
122 32 adantr N Fin R CRing M B s b B 0 s Y Ring
123 122 adantr N Fin R CRing M B s b B 0 s i 0 s Y Ring
124 simpll1 N Fin R CRing M B s b B 0 s i 0 s N Fin
125 40 adantr N Fin R CRing M B s b B 0 s i 0 s R Ring
126 simpll3 N Fin R CRing M B s b B 0 s i 0 s M B
127 5 1 2 3 4 mat2pmatbas N Fin R Ring M B T M Base Y
128 124 125 126 127 syl3anc N Fin R CRing M B s b B 0 s i 0 s T M Base Y
129 87 adantr N Fin R CRing M B s b B 0 s i 0 s s 0
130 simprr N Fin R CRing M B s b B 0 s b B 0 s
131 130 anim1i N Fin R CRing M B s b B 0 s i 0 s b B 0 s i 0 s
132 1 2 3 4 5 m2pmfzmap N Fin R Ring s 0 b B 0 s i 0 s T b i Base Y
133 124 125 129 131 132 syl31anc N Fin R CRing M B s b B 0 s i 0 s T b i Base Y
134 27 9 ringcl Y Ring T M Base Y T b i Base Y T M × ˙ T b i Base Y
135 123 128 133 134 syl3anc N Fin R CRing M B s b B 0 s i 0 s T M × ˙ T b i Base Y
136 eqid Scalar Y = Scalar Y
137 eqid Base Scalar Y = Base Scalar Y
138 27 136 8 137 lmodvscl Y LMod i × ˙ X Base Scalar Y T M × ˙ T b i Base Y i × ˙ X · ˙ T M × ˙ T b i Base Y
139 92 121 135 138 syl3anc N Fin R CRing M B s b B 0 s i 0 s i × ˙ X · ˙ T M × ˙ T b i Base Y
140 27 11 35 87 139 gsummptfzsplitl N Fin R CRing M B s b B 0 s Y i = 0 s i × ˙ X · ˙ T M × ˙ T b i = Y i = 1 s i × ˙ X · ˙ T M × ˙ T b i + ˙ Y i 0 i × ˙ X · ˙ T M × ˙ T b i
141 0nn0 0 0
142 141 a1i N Fin R CRing M B s b B 0 s 0 0
143 eqid 0 mulGrp P = 0 mulGrp P
144 95 143 7 mulg0 X Base P 0 × ˙ X = 0 mulGrp P
145 107 144 syl N Fin R CRing M B 0 × ˙ X = 0 mulGrp P
146 145 adantr N Fin R CRing M B s b B 0 s 0 × ˙ X = 0 mulGrp P
147 146 oveq1d N Fin R CRing M B s b B 0 s 0 × ˙ X · ˙ T M × ˙ T b 0 = 0 mulGrp P · ˙ T M × ˙ T b 0
148 eqid 1 P = 1 P
149 93 148 ringidval 1 P = 0 mulGrp P
150 149 a1i N Fin R CRing M B s b B 0 s 1 P = 0 mulGrp P
151 150 eqcomd N Fin R CRing M B s b B 0 s 0 mulGrp P = 1 P
152 151 oveq1d N Fin R CRing M B s b B 0 s 0 mulGrp P · ˙ T M × ˙ T b 0 = 1 P · ˙ T M × ˙ T b 0
153 115 adantr N Fin R CRing M B s b B 0 s P = Scalar Y
154 153 fveq2d N Fin R CRing M B s b B 0 s 1 P = 1 Scalar Y
155 154 oveq1d N Fin R CRing M B s b B 0 s 1 P · ˙ T M × ˙ T b 0 = 1 Scalar Y · ˙ T M × ˙ T b 0
156 28 127 syl3an2 N Fin R CRing M B T M Base Y
157 156 adantr N Fin R CRing M B s b B 0 s T M Base Y
158 simpl b : 0 s B s b : 0 s B
159 elnn0uz s 0 s 0
160 13 159 sylib s s 0
161 eluzfz1 s 0 0 0 s
162 160 161 syl s 0 0 s
163 162 adantl b : 0 s B s 0 0 s
164 158 163 ffvelcdmd b : 0 s B s b 0 B
165 164 ex b : 0 s B s b 0 B
166 42 165 syl b B 0 s s b 0 B
167 166 impcom s b B 0 s b 0 B
168 167 adantl N Fin R CRing M B s b B 0 s b 0 B
169 5 1 2 3 4 mat2pmatbas N Fin R Ring b 0 B T b 0 Base Y
170 60 40 168 169 syl3anc N Fin R CRing M B s b B 0 s T b 0 Base Y
171 27 9 ringcl Y Ring T M Base Y T b 0 Base Y T M × ˙ T b 0 Base Y
172 122 157 170 171 syl3anc N Fin R CRing M B s b B 0 s T M × ˙ T b 0 Base Y
173 eqid 1 Scalar Y = 1 Scalar Y
174 27 136 8 173 lmodvs1 Y LMod T M × ˙ T b 0 Base Y 1 Scalar Y · ˙ T M × ˙ T b 0 = T M × ˙ T b 0
175 91 172 174 syl2anc N Fin R CRing M B s b B 0 s 1 Scalar Y · ˙ T M × ˙ T b 0 = T M × ˙ T b 0
176 155 175 eqtrd N Fin R CRing M B s b B 0 s 1 P · ˙ T M × ˙ T b 0 = T M × ˙ T b 0
177 147 152 176 3eqtrd N Fin R CRing M B s b B 0 s 0 × ˙ X · ˙ T M × ˙ T b 0 = T M × ˙ T b 0
178 177 172 eqeltrd N Fin R CRing M B s b B 0 s 0 × ˙ X · ˙ T M × ˙ T b 0 Base Y
179 oveq1 i = 0 i × ˙ X = 0 × ˙ X
180 2fveq3 i = 0 T b i = T b 0
181 180 oveq2d i = 0 T M × ˙ T b i = T M × ˙ T b 0
182 179 181 oveq12d i = 0 i × ˙ X · ˙ T M × ˙ T b i = 0 × ˙ X · ˙ T M × ˙ T b 0
183 182 adantl N Fin R CRing M B s b B 0 s i = 0 i × ˙ X · ˙ T M × ˙ T b i = 0 × ˙ X · ˙ T M × ˙ T b 0
184 27 58 142 178 183 gsumsnd N Fin R CRing M B s b B 0 s Y i 0 i × ˙ X · ˙ T M × ˙ T b i = 0 × ˙ X · ˙ T M × ˙ T b 0
185 95 149 7 mulg0 X Base P 0 × ˙ X = 1 P
186 107 185 syl N Fin R CRing M B 0 × ˙ X = 1 P
187 186 adantr N Fin R CRing M B s b B 0 s 0 × ˙ X = 1 P
188 187 oveq1d N Fin R CRing M B s b B 0 s 0 × ˙ X · ˙ T M × ˙ T b 0 = 1 P · ˙ T M × ˙ T b 0
189 184 188 176 3eqtrd N Fin R CRing M B s b B 0 s Y i 0 i × ˙ X · ˙ T M × ˙ T b i = T M × ˙ T b 0
190 189 oveq2d N Fin R CRing M B s b B 0 s Y i = 1 s i × ˙ X · ˙ T M × ˙ T b i + ˙ Y i 0 i × ˙ X · ˙ T M × ˙ T b i = Y i = 1 s i × ˙ X · ˙ T M × ˙ T b i + ˙ T M × ˙ T b 0
191 140 190 eqtrd N Fin R CRing M B s b B 0 s Y i = 0 s i × ˙ X · ˙ T M × ˙ T b i = Y i = 1 s i × ˙ X · ˙ T M × ˙ T b i + ˙ T M × ˙ T b 0
192 86 191 oveq12d N Fin R CRing M B s b B 0 s Y i = 0 s i + 1 × ˙ X · ˙ T b i - ˙ Y i = 0 s i × ˙ X · ˙ T M × ˙ T b i = Y i = 0 s 1 i + 1 × ˙ X · ˙ T b i + ˙ s + 1 × ˙ X · ˙ T b s - ˙ Y i = 1 s i × ˙ X · ˙ T M × ˙ T b i + ˙ T M × ˙ T b 0
193 fzfid N Fin R CRing M B s b B 0 s 0 s 1 Fin
194 simpll1 N Fin R CRing M B s b B 0 s i 0 s 1 N Fin
195 40 adantr N Fin R CRing M B s b B 0 s i 0 s 1 R Ring
196 42 adantl s b B 0 s b : 0 s B
197 196 adantr s b B 0 s i 0 s 1 b : 0 s B
198 nnz s s
199 fzoval s 0 ..^ s = 0 s 1
200 198 199 syl s 0 ..^ s = 0 s 1
201 200 eqcomd s 0 s 1 = 0 ..^ s
202 201 eleq2d s i 0 s 1 i 0 ..^ s
203 elfzofz i 0 ..^ s i 0 s
204 202 203 biimtrdi s i 0 s 1 i 0 s
205 204 adantr s b B 0 s i 0 s 1 i 0 s
206 205 imp s b B 0 s i 0 s 1 i 0 s
207 197 206 ffvelcdmd s b B 0 s i 0 s 1 b i B
208 207 adantll N Fin R CRing M B s b B 0 s i 0 s 1 b i B
209 elfznn0 i 0 s 1 i 0
210 209 adantl N Fin R CRing M B s b B 0 s i 0 s 1 i 0
211 50 a1i N Fin R CRing M B s b B 0 s i 0 s 1 1 0
212 210 211 nn0addcld N Fin R CRing M B s b B 0 s i 0 s 1 i + 1 0
213 194 195 208 212 53 syl22anc N Fin R CRing M B s b B 0 s i 0 s 1 i + 1 × ˙ X · ˙ T b i Base Y
214 213 ralrimiva N Fin R CRing M B s b B 0 s i 0 s 1 i + 1 × ˙ X · ˙ T b i Base Y
215 27 35 193 214 gsummptcl N Fin R CRing M B s b B 0 s Y i = 0 s 1 i + 1 × ˙ X · ˙ T b i Base Y
216 27 11 cmncom Y CMnd Y i = 0 s 1 i + 1 × ˙ X · ˙ T b i Base Y s + 1 × ˙ X · ˙ T b s Base Y Y i = 0 s 1 i + 1 × ˙ X · ˙ T b i + ˙ s + 1 × ˙ X · ˙ T b s = s + 1 × ˙ X · ˙ T b s + ˙ Y i = 0 s 1 i + 1 × ˙ X · ˙ T b i
217 35 215 71 216 syl3anc N Fin R CRing M B s b B 0 s Y i = 0 s 1 i + 1 × ˙ X · ˙ T b i + ˙ s + 1 × ˙ X · ˙ T b s = s + 1 × ˙ X · ˙ T b s + ˙ Y i = 0 s 1 i + 1 × ˙ X · ˙ T b i
218 217 oveq1d N Fin R CRing M B s b B 0 s Y i = 0 s 1 i + 1 × ˙ X · ˙ T b i + ˙ s + 1 × ˙ X · ˙ T b s - ˙ Y i = 1 s i × ˙ X · ˙ T M × ˙ T b i + ˙ T M × ˙ T b 0 = s + 1 × ˙ X · ˙ T b s + ˙ Y i = 0 s 1 i + 1 × ˙ X · ˙ T b i - ˙ Y i = 1 s i × ˙ X · ˙ T M × ˙ T b i + ˙ T M × ˙ T b 0
219 ringgrp Y Ring Y Grp
220 32 219 syl N Fin R CRing M B Y Grp
221 220 adantr N Fin R CRing M B s b B 0 s Y Grp
222 fzfid N Fin R CRing M B s b B 0 s 1 s Fin
223 91 adantr N Fin R CRing M B s b B 0 s i 1 s Y LMod
224 101 adantr N Fin R CRing M B s b B 0 s i 1 s mulGrp P Mnd
225 elfznn i 1 s i
226 225 nnnn0d i 1 s i 0
227 226 adantl N Fin R CRing M B s b B 0 s i 1 s i 0
228 108 adantr N Fin R CRing M B s b B 0 s i 1 s X Base P
229 95 7 224 227 228 mulgnn0cld N Fin R CRing M B s b B 0 s i 1 s i × ˙ X Base P
230 115 fveq2d N Fin R CRing M B Base P = Base Scalar Y
231 230 adantr N Fin R CRing M B s b B 0 s Base P = Base Scalar Y
232 231 adantr N Fin R CRing M B s b B 0 s i 1 s Base P = Base Scalar Y
233 229 232 eleqtrd N Fin R CRing M B s b B 0 s i 1 s i × ˙ X Base Scalar Y
234 122 adantr N Fin R CRing M B s b B 0 s i 1 s Y Ring
235 157 adantr N Fin R CRing M B s b B 0 s i 1 s T M Base Y
236 simpll1 N Fin R CRing M B s b B 0 s i 1 s N Fin
237 40 adantr N Fin R CRing M B s b B 0 s i 1 s R Ring
238 196 adantl N Fin R CRing M B s b B 0 s b : 0 s B
239 238 adantr N Fin R CRing M B s b B 0 s i 1 s b : 0 s B
240 1eluzge0 1 0
241 fzss1 1 0 1 s 0 s
242 240 241 mp1i s 1 s 0 s
243 242 sseld s i 1 s i 0 s
244 243 ad2antrl N Fin R CRing M B s b B 0 s i 1 s i 0 s
245 244 imp N Fin R CRing M B s b B 0 s i 1 s i 0 s
246 239 245 ffvelcdmd N Fin R CRing M B s b B 0 s i 1 s b i B
247 5 1 2 3 4 mat2pmatbas N Fin R Ring b i B T b i Base Y
248 236 237 246 247 syl3anc N Fin R CRing M B s b B 0 s i 1 s T b i Base Y
249 234 235 248 134 syl3anc N Fin R CRing M B s b B 0 s i 1 s T M × ˙ T b i Base Y
250 223 233 249 138 syl3anc N Fin R CRing M B s b B 0 s i 1 s i × ˙ X · ˙ T M × ˙ T b i Base Y
251 250 ralrimiva N Fin R CRing M B s b B 0 s i 1 s i × ˙ X · ˙ T M × ˙ T b i Base Y
252 27 35 222 251 gsummptcl N Fin R CRing M B s b B 0 s Y i = 1 s i × ˙ X · ˙ T M × ˙ T b i Base Y
253 27 11 12 grpaddsubass Y Grp s + 1 × ˙ X · ˙ T b s Base Y Y i = 0 s 1 i + 1 × ˙ X · ˙ T b i Base Y Y i = 1 s i × ˙ X · ˙ T M × ˙ T b i Base Y s + 1 × ˙ X · ˙ T b s + ˙ Y i = 0 s 1 i + 1 × ˙ X · ˙ T b i - ˙ Y i = 1 s i × ˙ X · ˙ T M × ˙ T b i = s + 1 × ˙ X · ˙ T b s + ˙ Y i = 0 s 1 i + 1 × ˙ X · ˙ T b i - ˙ Y i = 1 s i × ˙ X · ˙ T M × ˙ T b i
254 221 71 215 252 253 syl13anc N Fin R CRing M B s b B 0 s s + 1 × ˙ X · ˙ T b s + ˙ Y i = 0 s 1 i + 1 × ˙ X · ˙ T b i - ˙ Y i = 1 s i × ˙ X · ˙ T M × ˙ T b i = s + 1 × ˙ X · ˙ T b s + ˙ Y i = 0 s 1 i + 1 × ˙ X · ˙ T b i - ˙ Y i = 1 s i × ˙ X · ˙ T M × ˙ T b i
255 oveq1 x = i x 1 = i 1
256 255 oveq1d x = i x - 1 + 1 = i - 1 + 1
257 256 oveq1d x = i x - 1 + 1 × ˙ X = i - 1 + 1 × ˙ X
258 255 fveq2d x = i b x 1 = b i 1
259 258 fveq2d x = i T b x 1 = T b i 1
260 257 259 oveq12d x = i x - 1 + 1 × ˙ X · ˙ T b x 1 = i - 1 + 1 × ˙ X · ˙ T b i 1
261 260 cbvmptv x 1 s x - 1 + 1 × ˙ X · ˙ T b x 1 = i 1 s i - 1 + 1 × ˙ X · ˙ T b i 1
262 225 nncnd i 1 s i
263 262 adantl s i 1 s i
264 npcan1 i i - 1 + 1 = i
265 263 264 syl s i 1 s i - 1 + 1 = i
266 265 oveq1d s i 1 s i - 1 + 1 × ˙ X = i × ˙ X
267 266 oveq1d s i 1 s i - 1 + 1 × ˙ X · ˙ T b i 1 = i × ˙ X · ˙ T b i 1
268 267 mpteq2dva s i 1 s i - 1 + 1 × ˙ X · ˙ T b i 1 = i 1 s i × ˙ X · ˙ T b i 1
269 261 268 eqtrid s x 1 s x - 1 + 1 × ˙ X · ˙ T b x 1 = i 1 s i × ˙ X · ˙ T b i 1
270 269 oveq2d s Y x = 1 s x - 1 + 1 × ˙ X · ˙ T b x 1 = Y i = 1 s i × ˙ X · ˙ T b i 1
271 270 ad2antrl N Fin R CRing M B s b B 0 s Y x = 1 s x - 1 + 1 × ˙ X · ˙ T b x 1 = Y i = 1 s i × ˙ X · ˙ T b i 1
272 271 oveq1d N Fin R CRing M B s b B 0 s Y x = 1 s x - 1 + 1 × ˙ X · ˙ T b x 1 - ˙ Y i = 1 s i × ˙ X · ˙ T M × ˙ T b i = Y i = 1 s i × ˙ X · ˙ T b i 1 - ˙ Y i = 1 s i × ˙ X · ˙ T M × ˙ T b i
273 eqid 0 Y = 0 Y
274 1zzd N Fin R CRing M B s b B 0 s 1
275 0zd N Fin R CRing M B s b B 0 s 0
276 37 nn0zd N Fin R CRing M B s b B 0 s s 1
277 oveq1 i = x 1 i + 1 = x - 1 + 1
278 277 oveq1d i = x 1 i + 1 × ˙ X = x - 1 + 1 × ˙ X
279 2fveq3 i = x 1 T b i = T b x 1
280 278 279 oveq12d i = x 1 i + 1 × ˙ X · ˙ T b i = x - 1 + 1 × ˙ X · ˙ T b x 1
281 27 273 35 274 275 276 213 280 gsummptshft N Fin R CRing M B s b B 0 s Y i = 0 s 1 i + 1 × ˙ X · ˙ T b i = Y x = 0 + 1 s - 1 + 1 x - 1 + 1 × ˙ X · ˙ T b x 1
282 0p1e1 0 + 1 = 1
283 282 a1i N Fin R CRing M B s b B 0 s 0 + 1 = 1
284 76 ad2antrl N Fin R CRing M B s b B 0 s s - 1 + 1 = s
285 283 284 oveq12d N Fin R CRing M B s b B 0 s 0 + 1 s - 1 + 1 = 1 s
286 285 mpteq1d N Fin R CRing M B s b B 0 s x 0 + 1 s - 1 + 1 x - 1 + 1 × ˙ X · ˙ T b x 1 = x 1 s x - 1 + 1 × ˙ X · ˙ T b x 1
287 286 oveq2d N Fin R CRing M B s b B 0 s Y x = 0 + 1 s - 1 + 1 x - 1 + 1 × ˙ X · ˙ T b x 1 = Y x = 1 s x - 1 + 1 × ˙ X · ˙ T b x 1
288 281 287 eqtrd N Fin R CRing M B s b B 0 s Y i = 0 s 1 i + 1 × ˙ X · ˙ T b i = Y x = 1 s x - 1 + 1 × ˙ X · ˙ T b x 1
289 288 oveq1d N Fin R CRing M B s b B 0 s Y i = 0 s 1 i + 1 × ˙ X · ˙ T b i - ˙ Y i = 1 s i × ˙ X · ˙ T M × ˙ T b i = Y x = 1 s x - 1 + 1 × ˙ X · ˙ T b x 1 - ˙ Y i = 1 s i × ˙ X · ˙ T M × ˙ T b i
290 ringabl Y Ring Y Abel
291 32 290 syl N Fin R CRing M B Y Abel
292 291 adantr N Fin R CRing M B s b B 0 s Y Abel
293 225 adantl s i 1 s i
294 nnz i i
295 elfzm1b i s i 1 s i 1 0 s 1
296 294 198 295 syl2an i s i 1 s i 1 0 s 1
297 200 adantl i s 0 ..^ s = 0 s 1
298 297 eqcomd i s 0 s 1 = 0 ..^ s
299 298 eleq2d i s i 1 0 s 1 i 1 0 ..^ s
300 elfzofz i 1 0 ..^ s i 1 0 s
301 299 300 biimtrdi i s i 1 0 s 1 i 1 0 s
302 296 301 sylbid i s i 1 s i 1 0 s
303 302 expimpd i s i 1 s i 1 0 s
304 293 303 mpcom s i 1 s i 1 0 s
305 304 ex s i 1 s i 1 0 s
306 305 ad2antrl N Fin R CRing M B s b B 0 s i 1 s i 1 0 s
307 306 imp N Fin R CRing M B s b B 0 s i 1 s i 1 0 s
308 239 307 ffvelcdmd N Fin R CRing M B s b B 0 s i 1 s b i 1 B
309 1 2 5 3 4 27 8 7 6 mat2pmatscmxcl N Fin R Ring b i 1 B i 0 i × ˙ X · ˙ T b i 1 Base Y
310 236 237 308 227 309 syl22anc N Fin R CRing M B s b B 0 s i 1 s i × ˙ X · ˙ T b i 1 Base Y
311 eqid i 1 s i × ˙ X · ˙ T b i 1 = i 1 s i × ˙ X · ˙ T b i 1
312 eqid i 1 s i × ˙ X · ˙ T M × ˙ T b i = i 1 s i × ˙ X · ˙ T M × ˙ T b i
313 27 12 292 222 310 250 311 312 gsummptfidmsub N Fin R CRing M B s b B 0 s Y i = 1 s i × ˙ X · ˙ T b i 1 - ˙ i × ˙ X · ˙ T M × ˙ T b i = Y i = 1 s i × ˙ X · ˙ T b i 1 - ˙ Y i = 1 s i × ˙ X · ˙ T M × ˙ T b i
314 272 289 313 3eqtr4d N Fin R CRing M B s b B 0 s Y i = 0 s 1 i + 1 × ˙ X · ˙ T b i - ˙ Y i = 1 s i × ˙ X · ˙ T M × ˙ T b i = Y i = 1 s i × ˙ X · ˙ T b i 1 - ˙ i × ˙ X · ˙ T M × ˙ T b i
315 314 oveq2d N Fin R CRing M B s b B 0 s s + 1 × ˙ X · ˙ T b s + ˙ Y i = 0 s 1 i + 1 × ˙ X · ˙ T b i - ˙ Y i = 1 s i × ˙ X · ˙ T M × ˙ T b i = s + 1 × ˙ X · ˙ T b s + ˙ Y i = 1 s i × ˙ X · ˙ T b i 1 - ˙ i × ˙ X · ˙ T M × ˙ T b i
316 221 adantr N Fin R CRing M B s b B 0 s i 1 s Y Grp
317 27 12 grpsubcl Y Grp i × ˙ X · ˙ T b i 1 Base Y i × ˙ X · ˙ T M × ˙ T b i Base Y i × ˙ X · ˙ T b i 1 - ˙ i × ˙ X · ˙ T M × ˙ T b i Base Y
318 316 310 250 317 syl3anc N Fin R CRing M B s b B 0 s i 1 s i × ˙ X · ˙ T b i 1 - ˙ i × ˙ X · ˙ T M × ˙ T b i Base Y
319 318 ralrimiva N Fin R CRing M B s b B 0 s i 1 s i × ˙ X · ˙ T b i 1 - ˙ i × ˙ X · ˙ T M × ˙ T b i Base Y
320 27 35 222 319 gsummptcl N Fin R CRing M B s b B 0 s Y i = 1 s i × ˙ X · ˙ T b i 1 - ˙ i × ˙ X · ˙ T M × ˙ T b i Base Y
321 27 11 cmncom Y CMnd s + 1 × ˙ X · ˙ T b s Base Y Y i = 1 s i × ˙ X · ˙ T b i 1 - ˙ i × ˙ X · ˙ T M × ˙ T b i Base Y s + 1 × ˙ X · ˙ T b s + ˙ Y i = 1 s i × ˙ X · ˙ T b i 1 - ˙ i × ˙ X · ˙ T M × ˙ T b i = Y i = 1 s i × ˙ X · ˙ T b i 1 - ˙ i × ˙ X · ˙ T M × ˙ T b i + ˙ s + 1 × ˙ X · ˙ T b s
322 35 71 320 321 syl3anc N Fin R CRing M B s b B 0 s s + 1 × ˙ X · ˙ T b s + ˙ Y i = 1 s i × ˙ X · ˙ T b i 1 - ˙ i × ˙ X · ˙ T M × ˙ T b i = Y i = 1 s i × ˙ X · ˙ T b i 1 - ˙ i × ˙ X · ˙ T M × ˙ T b i + ˙ s + 1 × ˙ X · ˙ T b s
323 254 315 322 3eqtrd N Fin R CRing M B s b B 0 s s + 1 × ˙ X · ˙ T b s + ˙ Y i = 0 s 1 i + 1 × ˙ X · ˙ T b i - ˙ Y i = 1 s i × ˙ X · ˙ T M × ˙ T b i = Y i = 1 s i × ˙ X · ˙ T b i 1 - ˙ i × ˙ X · ˙ T M × ˙ T b i + ˙ s + 1 × ˙ X · ˙ T b s
324 323 oveq1d N Fin R CRing M B s b B 0 s s + 1 × ˙ X · ˙ T b s + ˙ Y i = 0 s 1 i + 1 × ˙ X · ˙ T b i - ˙ Y i = 1 s i × ˙ X · ˙ T M × ˙ T b i - ˙ T M × ˙ T b 0 = Y i = 1 s i × ˙ X · ˙ T b i 1 - ˙ i × ˙ X · ˙ T M × ˙ T b i + ˙ s + 1 × ˙ X · ˙ T b s - ˙ T M × ˙ T b 0
325 27 11 mndcl Y Mnd s + 1 × ˙ X · ˙ T b s Base Y Y i = 0 s 1 i + 1 × ˙ X · ˙ T b i Base Y s + 1 × ˙ X · ˙ T b s + ˙ Y i = 0 s 1 i + 1 × ˙ X · ˙ T b i Base Y
326 58 71 215 325 syl3anc N Fin R CRing M B s b B 0 s s + 1 × ˙ X · ˙ T b s + ˙ Y i = 0 s 1 i + 1 × ˙ X · ˙ T b i Base Y
327 27 11 12 292 326 252 172 ablsubsub4 N Fin R CRing M B s b B 0 s s + 1 × ˙ X · ˙ T b s + ˙ Y i = 0 s 1 i + 1 × ˙ X · ˙ T b i - ˙ Y i = 1 s i × ˙ X · ˙ T M × ˙ T b i - ˙ T M × ˙ T b 0 = s + 1 × ˙ X · ˙ T b s + ˙ Y i = 0 s 1 i + 1 × ˙ X · ˙ T b i - ˙ Y i = 1 s i × ˙ X · ˙ T M × ˙ T b i + ˙ T M × ˙ T b 0
328 27 11 12 grpaddsubass Y Grp Y i = 1 s i × ˙ X · ˙ T b i 1 - ˙ i × ˙ X · ˙ T M × ˙ T b i Base Y s + 1 × ˙ X · ˙ T b s Base Y T M × ˙ T b 0 Base Y Y i = 1 s i × ˙ X · ˙ T b i 1 - ˙ i × ˙ X · ˙ T M × ˙ T b i + ˙ s + 1 × ˙ X · ˙ T b s - ˙ T M × ˙ T b 0 = Y i = 1 s i × ˙ X · ˙ T b i 1 - ˙ i × ˙ X · ˙ T M × ˙ T b i + ˙ s + 1 × ˙ X · ˙ T b s - ˙ T M × ˙ T b 0
329 221 320 71 172 328 syl13anc N Fin R CRing M B s b B 0 s Y i = 1 s i × ˙ X · ˙ T b i 1 - ˙ i × ˙ X · ˙ T M × ˙ T b i + ˙ s + 1 × ˙ X · ˙ T b s - ˙ T M × ˙ T b 0 = Y i = 1 s i × ˙ X · ˙ T b i 1 - ˙ i × ˙ X · ˙ T M × ˙ T b i + ˙ s + 1 × ˙ X · ˙ T b s - ˙ T M × ˙ T b 0
330 324 327 329 3eqtr3d N Fin R CRing M B s b B 0 s s + 1 × ˙ X · ˙ T b s + ˙ Y i = 0 s 1 i + 1 × ˙ X · ˙ T b i - ˙ Y i = 1 s i × ˙ X · ˙ T M × ˙ T b i + ˙ T M × ˙ T b 0 = Y i = 1 s i × ˙ X · ˙ T b i 1 - ˙ i × ˙ X · ˙ T M × ˙ T b i + ˙ s + 1 × ˙ X · ˙ T b s - ˙ T M × ˙ T b 0
331 5 1 2 3 4 mat2pmatbas N Fin R Ring b i 1 B T b i 1 Base Y
332 236 237 308 331 syl3anc N Fin R CRing M B s b B 0 s i 1 s T b i 1 Base Y
333 27 8 136 137 12 223 233 332 249 lmodsubdi N Fin R CRing M B s b B 0 s i 1 s i × ˙ X · ˙ T b i 1 - ˙ T M × ˙ T b i = i × ˙ X · ˙ T b i 1 - ˙ i × ˙ X · ˙ T M × ˙ T b i
334 333 eqcomd N Fin R CRing M B s b B 0 s i 1 s i × ˙ X · ˙ T b i 1 - ˙ i × ˙ X · ˙ T M × ˙ T b i = i × ˙ X · ˙ T b i 1 - ˙ T M × ˙ T b i
335 334 mpteq2dva N Fin R CRing M B s b B 0 s i 1 s i × ˙ X · ˙ T b i 1 - ˙ i × ˙ X · ˙ T M × ˙ T b i = i 1 s i × ˙ X · ˙ T b i 1 - ˙ T M × ˙ T b i
336 335 oveq2d N Fin R CRing M B s b B 0 s Y i = 1 s i × ˙ X · ˙ T b i 1 - ˙ i × ˙ X · ˙ T M × ˙ T b i = Y i = 1 s i × ˙ X · ˙ T b i 1 - ˙ T M × ˙ T b i
337 336 oveq1d N Fin R CRing M B s b B 0 s Y i = 1 s i × ˙ X · ˙ T b i 1 - ˙ i × ˙ X · ˙ T M × ˙ T b i + ˙ s + 1 × ˙ X · ˙ T b s - ˙ T M × ˙ T b 0 = Y i = 1 s i × ˙ X · ˙ T b i 1 - ˙ T M × ˙ T b i + ˙ s + 1 × ˙ X · ˙ T b s - ˙ T M × ˙ T b 0
338 218 330 337 3eqtrd N Fin R CRing M B s b B 0 s Y i = 0 s 1 i + 1 × ˙ X · ˙ T b i + ˙ s + 1 × ˙ X · ˙ T b s - ˙ Y i = 1 s i × ˙ X · ˙ T M × ˙ T b i + ˙ T M × ˙ T b 0 = Y i = 1 s i × ˙ X · ˙ T b i 1 - ˙ T M × ˙ T b i + ˙ s + 1 × ˙ X · ˙ T b s - ˙ T M × ˙ T b 0
339 18 192 338 3eqtrd N Fin R CRing M B s b B 0 s X · ˙ 1 ˙ × ˙ Y i = 0 s i × ˙ X · ˙ T b i - ˙ T M × ˙ Y i = 0 s i × ˙ X · ˙ T b i = Y i = 1 s i × ˙ X · ˙ T b i 1 - ˙ T M × ˙ T b i + ˙ s + 1 × ˙ X · ˙ T b s - ˙ T M × ˙ T b 0