Metamath Proof Explorer


Theorem matunitlindflem2

Description: One direction of matunitlindf . (Contributed by Brendan Leahy, 2-Jun-2021)

Ref Expression
Assertion matunitlindflem2 R Field M Base I Mat R I curry M LIndF R freeLMod I I maDet R M Unit R

Proof

Step Hyp Ref Expression
1 eqid I Mat R = I Mat R
2 eqid Base I Mat R = Base I Mat R
3 1 2 matrcl M Base I Mat R I Fin R V
4 3 simpld M Base I Mat R I Fin
5 4 ad3antlr R Field M Base I Mat R I curry M LIndF R freeLMod I I Fin
6 isfld R Field R DivRing R CRing
7 6 simplbi R Field R DivRing
8 7 anim1i R Field M Base I Mat R R DivRing M Base I Mat R
9 4 ad2antrl R DivRing M Base I Mat R I I Fin
10 simpr R DivRing M Base I Mat R M Base I Mat R
11 xpfi I Fin I Fin I × I Fin
12 11 anidms I Fin I × I Fin
13 eqid R freeLMod I × I = R freeLMod I × I
14 eqid Base R = Base R
15 13 14 frlmfibas R DivRing I × I Fin Base R I × I = Base R freeLMod I × I
16 12 15 sylan2 R DivRing I Fin Base R I × I = Base R freeLMod I × I
17 1 13 matbas I Fin R DivRing Base R freeLMod I × I = Base I Mat R
18 17 ancoms R DivRing I Fin Base R freeLMod I × I = Base I Mat R
19 16 18 eqtrd R DivRing I Fin Base R I × I = Base I Mat R
20 19 eleq2d R DivRing I Fin M Base R I × I M Base I Mat R
21 4 20 sylan2 R DivRing M Base I Mat R M Base R I × I M Base I Mat R
22 fvex Base R V
23 4 4 11 syl2anc M Base I Mat R I × I Fin
24 elmapg Base R V I × I Fin M Base R I × I M : I × I Base R
25 22 23 24 sylancr M Base I Mat R M Base R I × I M : I × I Base R
26 25 adantl R DivRing M Base I Mat R M Base R I × I M : I × I Base R
27 21 26 bitr3d R DivRing M Base I Mat R M Base I Mat R M : I × I Base R
28 10 27 mpbid R DivRing M Base I Mat R M : I × I Base R
29 28 adantrr R DivRing M Base I Mat R I M : I × I Base R
30 eldifsn I Fin I Fin I
31 30 biimpri I Fin I I Fin
32 4 31 sylan M Base I Mat R I I Fin
33 32 adantl R DivRing M Base I Mat R I I Fin
34 curf M : I × I Base R I Fin Base R V curry M : I Base R I
35 22 34 mp3an3 M : I × I Base R I Fin curry M : I Base R I
36 29 33 35 syl2anc R DivRing M Base I Mat R I curry M : I Base R I
37 9 36 jca R DivRing M Base I Mat R I I Fin curry M : I Base R I
38 37 ex R DivRing M Base I Mat R I I Fin curry M : I Base R I
39 38 imdistani R DivRing M Base I Mat R I R DivRing I Fin curry M : I Base R I
40 39 anassrs R DivRing M Base I Mat R I R DivRing I Fin curry M : I Base R I
41 anass R DivRing I Fin curry M : I Base R I R DivRing I Fin curry M : I Base R I
42 40 41 sylibr R DivRing M Base I Mat R I R DivRing I Fin curry M : I Base R I
43 drngring R DivRing R Ring
44 eqid R unitVec I = R unitVec I
45 eqid R freeLMod I = R freeLMod I
46 eqid Base R freeLMod I = Base R freeLMod I
47 44 45 46 uvcff R Ring I Fin R unitVec I : I Base R freeLMod I
48 43 47 sylan R DivRing I Fin R unitVec I : I Base R freeLMod I
49 48 ffvelrnda R DivRing I Fin i I R unitVec I i Base R freeLMod I
50 49 ad4ant14 R DivRing I Fin curry M : I Base R I curry M LIndF R freeLMod I i I R unitVec I i Base R freeLMod I
51 ffn curry M : I Base R I curry M Fn I
52 fnima curry M Fn I curry M I = ran curry M
53 51 52 syl curry M : I Base R I curry M I = ran curry M
54 53 adantl R DivRing I Fin curry M : I Base R I curry M I = ran curry M
55 54 fveq2d R DivRing I Fin curry M : I Base R I LSpan R freeLMod I curry M I = LSpan R freeLMod I ran curry M
56 55 adantr R DivRing I Fin curry M : I Base R I curry M LIndF R freeLMod I LSpan R freeLMod I curry M I = LSpan R freeLMod I ran curry M
57 simplll R DivRing I Fin curry M : I Base R I curry M LIndF R freeLMod I R DivRing
58 simpllr R DivRing I Fin curry M : I Base R I curry M LIndF R freeLMod I I Fin
59 45 frlmlmod R Ring I Fin R freeLMod I LMod
60 43 59 sylan R DivRing I Fin R freeLMod I LMod
61 60 adantr R DivRing I Fin curry M : I Base R I R freeLMod I LMod
62 lindfrn R freeLMod I LMod curry M LIndF R freeLMod I ran curry M LIndS R freeLMod I
63 61 62 sylan R DivRing I Fin curry M : I Base R I curry M LIndF R freeLMod I ran curry M LIndS R freeLMod I
64 45 frlmsca R DivRing I Fin R = Scalar R freeLMod I
65 drngnzr R DivRing R NzRing
66 65 adantr R DivRing I Fin R NzRing
67 64 66 eqeltrrd R DivRing I Fin Scalar R freeLMod I NzRing
68 60 67 jca R DivRing I Fin R freeLMod I LMod Scalar R freeLMod I NzRing
69 eqid Scalar R freeLMod I = Scalar R freeLMod I
70 46 69 lindff1 R freeLMod I LMod Scalar R freeLMod I NzRing curry M LIndF R freeLMod I curry M : dom curry M 1-1 Base R freeLMod I
71 70 3expa R freeLMod I LMod Scalar R freeLMod I NzRing curry M LIndF R freeLMod I curry M : dom curry M 1-1 Base R freeLMod I
72 68 71 sylan R DivRing I Fin curry M LIndF R freeLMod I curry M : dom curry M 1-1 Base R freeLMod I
73 fdm curry M : I Base R I dom curry M = I
74 f1eq2 dom curry M = I curry M : dom curry M 1-1 Base R freeLMod I curry M : I 1-1 Base R freeLMod I
75 74 biimpac curry M : dom curry M 1-1 Base R freeLMod I dom curry M = I curry M : I 1-1 Base R freeLMod I
76 72 73 75 syl2an R DivRing I Fin curry M LIndF R freeLMod I curry M : I Base R I curry M : I 1-1 Base R freeLMod I
77 76 an32s R DivRing I Fin curry M : I Base R I curry M LIndF R freeLMod I curry M : I 1-1 Base R freeLMod I
78 f1f1orn curry M : I 1-1 Base R freeLMod I curry M : I 1-1 onto ran curry M
79 77 78 syl R DivRing I Fin curry M : I Base R I curry M LIndF R freeLMod I curry M : I 1-1 onto ran curry M
80 f1oeng I Fin curry M : I 1-1 onto ran curry M I ran curry M
81 58 79 80 syl2anc R DivRing I Fin curry M : I Base R I curry M LIndF R freeLMod I I ran curry M
82 81 ensymd R DivRing I Fin curry M : I Base R I curry M LIndF R freeLMod I ran curry M I
83 lindsenlbs R DivRing I Fin ran curry M LIndS R freeLMod I ran curry M I ran curry M LBasis R freeLMod I
84 57 58 63 82 83 syl31anc R DivRing I Fin curry M : I Base R I curry M LIndF R freeLMod I ran curry M LBasis R freeLMod I
85 eqid LBasis R freeLMod I = LBasis R freeLMod I
86 eqid LSpan R freeLMod I = LSpan R freeLMod I
87 46 85 86 lbssp ran curry M LBasis R freeLMod I LSpan R freeLMod I ran curry M = Base R freeLMod I
88 84 87 syl R DivRing I Fin curry M : I Base R I curry M LIndF R freeLMod I LSpan R freeLMod I ran curry M = Base R freeLMod I
89 56 88 eqtrd R DivRing I Fin curry M : I Base R I curry M LIndF R freeLMod I LSpan R freeLMod I curry M I = Base R freeLMod I
90 89 adantr R DivRing I Fin curry M : I Base R I curry M LIndF R freeLMod I i I LSpan R freeLMod I curry M I = Base R freeLMod I
91 50 90 eleqtrrd R DivRing I Fin curry M : I Base R I curry M LIndF R freeLMod I i I R unitVec I i LSpan R freeLMod I curry M I
92 eqid Base Scalar R freeLMod I = Base Scalar R freeLMod I
93 eqid 0 Scalar R freeLMod I = 0 Scalar R freeLMod I
94 eqid R freeLMod I = R freeLMod I
95 45 14 frlmfibas R Ring I Fin Base R I = Base R freeLMod I
96 95 feq3d R Ring I Fin curry M : I Base R I curry M : I Base R freeLMod I
97 96 biimpa R Ring I Fin curry M : I Base R I curry M : I Base R freeLMod I
98 59 adantr R Ring I Fin curry M : I Base R I R freeLMod I LMod
99 simplr R Ring I Fin curry M : I Base R I I Fin
100 86 46 92 69 93 94 97 98 99 elfilspd R Ring I Fin curry M : I Base R I R unitVec I i LSpan R freeLMod I curry M I n Base Scalar R freeLMod I I R unitVec I i = R freeLMod I n R freeLMod I f curry M
101 45 frlmsca R Ring I Fin R = Scalar R freeLMod I
102 101 fveq2d R Ring I Fin Base R = Base Scalar R freeLMod I
103 102 oveq1d R Ring I Fin Base R I = Base Scalar R freeLMod I I
104 103 adantr R Ring I Fin curry M : I Base R I Base R I = Base Scalar R freeLMod I I
105 elmapi n Base R I n : I Base R
106 ffn n : I Base R n Fn I
107 106 adantl R Ring I Fin curry M : I Base R I n : I Base R n Fn I
108 51 ad2antlr R Ring I Fin curry M : I Base R I n : I Base R curry M Fn I
109 simpllr R Ring I Fin curry M : I Base R I n : I Base R I Fin
110 inidm I I = I
111 eqidd R Ring I Fin curry M : I Base R I n : I Base R k I n k = n k
112 eqidd R Ring I Fin curry M : I Base R I n : I Base R k I curry M k = curry M k
113 107 108 109 109 110 111 112 offval R Ring I Fin curry M : I Base R I n : I Base R n R freeLMod I f curry M = k I n k R freeLMod I curry M k
114 simp-4r R Ring I Fin curry M : I Base R I n : I Base R k I I Fin
115 ffvelrn n : I Base R k I n k Base R
116 115 adantll R Ring I Fin curry M : I Base R I n : I Base R k I n k Base R
117 ffvelrn curry M : I Base R I k I curry M k Base R I
118 117 ad4ant24 R Ring I Fin curry M : I Base R I n : I Base R k I curry M k Base R I
119 95 ad3antrrr R Ring I Fin curry M : I Base R I n : I Base R k I Base R I = Base R freeLMod I
120 118 119 eleqtrd R Ring I Fin curry M : I Base R I n : I Base R k I curry M k Base R freeLMod I
121 eqid R = R
122 45 46 14 114 116 120 94 121 frlmvscafval R Ring I Fin curry M : I Base R I n : I Base R k I n k R freeLMod I curry M k = I × n k R f curry M k
123 fvex n k V
124 fnconstg n k V I × n k Fn I
125 123 124 mp1i R Ring I Fin curry M : I Base R I n : I Base R k I I × n k Fn I
126 elmapfn curry M k Base R I curry M k Fn I
127 117 126 syl curry M : I Base R I k I curry M k Fn I
128 127 ad4ant24 R Ring I Fin curry M : I Base R I n : I Base R k I curry M k Fn I
129 123 fvconst2 j I I × n k j = n k
130 129 adantl R Ring I Fin curry M : I Base R I n : I Base R k I j I I × n k j = n k
131 eqidd R Ring I Fin curry M : I Base R I n : I Base R k I j I curry M k j = curry M k j
132 125 128 114 114 110 130 131 offval R Ring I Fin curry M : I Base R I n : I Base R k I I × n k R f curry M k = j I n k R curry M k j
133 122 132 eqtrd R Ring I Fin curry M : I Base R I n : I Base R k I n k R freeLMod I curry M k = j I n k R curry M k j
134 133 mpteq2dva R Ring I Fin curry M : I Base R I n : I Base R k I n k R freeLMod I curry M k = k I j I n k R curry M k j
135 113 134 eqtrd R Ring I Fin curry M : I Base R I n : I Base R n R freeLMod I f curry M = k I j I n k R curry M k j
136 135 oveq2d R Ring I Fin curry M : I Base R I n : I Base R R freeLMod I n R freeLMod I f curry M = R freeLMod I k I j I n k R curry M k j
137 eqid 0 R freeLMod I = 0 R freeLMod I
138 simplll R Ring I Fin curry M : I Base R I n : I Base R R Ring
139 simp-5l R Ring I Fin curry M : I Base R I n : I Base R k I j I R Ring
140 115 ad4ant23 R Ring I Fin curry M : I Base R I n : I Base R k I j I n k Base R
141 simplr R Ring I Fin curry M : I Base R I n : I Base R curry M : I Base R I
142 elmapi curry M k Base R I curry M k : I Base R
143 117 142 syl curry M : I Base R I k I curry M k : I Base R
144 143 ffvelrnda curry M : I Base R I k I j I curry M k j Base R
145 141 144 sylanl1 R Ring I Fin curry M : I Base R I n : I Base R k I j I curry M k j Base R
146 14 121 ringcl R Ring n k Base R curry M k j Base R n k R curry M k j Base R
147 139 140 145 146 syl3anc R Ring I Fin curry M : I Base R I n : I Base R k I j I n k R curry M k j Base R
148 147 fmpttd R Ring I Fin curry M : I Base R I n : I Base R k I j I n k R curry M k j : I Base R
149 elmapg Base R V I Fin j I n k R curry M k j Base R I j I n k R curry M k j : I Base R
150 22 149 mpan I Fin j I n k R curry M k j Base R I j I n k R curry M k j : I Base R
151 150 adantl R Ring I Fin j I n k R curry M k j Base R I j I n k R curry M k j : I Base R
152 95 eleq2d R Ring I Fin j I n k R curry M k j Base R I j I n k R curry M k j Base R freeLMod I
153 151 152 bitr3d R Ring I Fin j I n k R curry M k j : I Base R j I n k R curry M k j Base R freeLMod I
154 153 ad3antrrr R Ring I Fin curry M : I Base R I n : I Base R k I j I n k R curry M k j : I Base R j I n k R curry M k j Base R freeLMod I
155 148 154 mpbid R Ring I Fin curry M : I Base R I n : I Base R k I j I n k R curry M k j Base R freeLMod I
156 mptexg I Fin j I n k R curry M k j V
157 156 ralrimivw I Fin k I j I n k R curry M k j V
158 eqid k I j I n k R curry M k j = k I j I n k R curry M k j
159 158 fnmpt k I j I n k R curry M k j V k I j I n k R curry M k j Fn I
160 157 159 syl I Fin k I j I n k R curry M k j Fn I
161 id I Fin I Fin
162 fvexd I Fin 0 R freeLMod I V
163 160 161 162 fndmfifsupp I Fin finSupp 0 R freeLMod I k I j I n k R curry M k j
164 163 ad3antlr R Ring I Fin curry M : I Base R I n : I Base R finSupp 0 R freeLMod I k I j I n k R curry M k j
165 45 46 137 109 109 138 155 164 frlmgsum R Ring I Fin curry M : I Base R I n : I Base R R freeLMod I k I j I n k R curry M k j = j I R k I n k R curry M k j
166 136 165 eqtr2d R Ring I Fin curry M : I Base R I n : I Base R j I R k I n k R curry M k j = R freeLMod I n R freeLMod I f curry M
167 105 166 sylan2 R Ring I Fin curry M : I Base R I n Base R I j I R k I n k R curry M k j = R freeLMod I n R freeLMod I f curry M
168 167 eqeq2d R Ring I Fin curry M : I Base R I n Base R I R unitVec I i = j I R k I n k R curry M k j R unitVec I i = R freeLMod I n R freeLMod I f curry M
169 104 168 rexeqbidva R Ring I Fin curry M : I Base R I n Base R I R unitVec I i = j I R k I n k R curry M k j n Base Scalar R freeLMod I I R unitVec I i = R freeLMod I n R freeLMod I f curry M
170 100 169 bitr4d R Ring I Fin curry M : I Base R I R unitVec I i LSpan R freeLMod I curry M I n Base R I R unitVec I i = j I R k I n k R curry M k j
171 43 170 sylanl1 R DivRing I Fin curry M : I Base R I R unitVec I i LSpan R freeLMod I curry M I n Base R I R unitVec I i = j I R k I n k R curry M k j
172 171 ad2antrr R DivRing I Fin curry M : I Base R I curry M LIndF R freeLMod I i I R unitVec I i LSpan R freeLMod I curry M I n Base R I R unitVec I i = j I R k I n k R curry M k j
173 91 172 mpbid R DivRing I Fin curry M : I Base R I curry M LIndF R freeLMod I i I n Base R I R unitVec I i = j I R k I n k R curry M k j
174 173 ralrimiva R DivRing I Fin curry M : I Base R I curry M LIndF R freeLMod I i I n Base R I R unitVec I i = j I R k I n k R curry M k j
175 42 174 sylan R DivRing M Base I Mat R I curry M LIndF R freeLMod I i I n Base R I R unitVec I i = j I R k I n k R curry M k j
176 10 21 mpbird R DivRing M Base I Mat R M Base R I × I
177 elmapfn M Base R I × I M Fn I × I
178 176 177 syl R DivRing M Base I Mat R M Fn I × I
179 4 adantl R DivRing M Base I Mat R I Fin
180 an32 M Fn I × I j I k I M Fn I × I k I j I
181 df-3an M Fn I × I k I j I M Fn I × I k I j I
182 180 181 bitr4i M Fn I × I j I k I M Fn I × I k I j I
183 curfv M Fn I × I k I j I I Fin curry M k j = k M j
184 182 183 sylanb M Fn I × I j I k I I Fin curry M k j = k M j
185 184 an32s M Fn I × I j I I Fin k I curry M k j = k M j
186 185 oveq2d M Fn I × I j I I Fin k I n k R curry M k j = n k R k M j
187 186 mpteq2dva M Fn I × I j I I Fin k I n k R curry M k j = k I n k R k M j
188 187 an32s M Fn I × I I Fin j I k I n k R curry M k j = k I n k R k M j
189 188 oveq2d M Fn I × I I Fin j I R k I n k R curry M k j = R k I n k R k M j
190 189 mpteq2dva M Fn I × I I Fin j I R k I n k R curry M k j = j I R k I n k R k M j
191 190 eqeq2d M Fn I × I I Fin R unitVec I i = j I R k I n k R curry M k j R unitVec I i = j I R k I n k R k M j
192 191 rexbidv M Fn I × I I Fin n Base R I R unitVec I i = j I R k I n k R curry M k j n Base R I R unitVec I i = j I R k I n k R k M j
193 192 ralbidv M Fn I × I I Fin i I n Base R I R unitVec I i = j I R k I n k R curry M k j i I n Base R I R unitVec I i = j I R k I n k R k M j
194 178 179 193 syl2anc R DivRing M Base I Mat R i I n Base R I R unitVec I i = j I R k I n k R curry M k j i I n Base R I R unitVec I i = j I R k I n k R k M j
195 194 ad2antrr R DivRing M Base I Mat R I curry M LIndF R freeLMod I i I n Base R I R unitVec I i = j I R k I n k R curry M k j i I n Base R I R unitVec I i = j I R k I n k R k M j
196 175 195 mpbid R DivRing M Base I Mat R I curry M LIndF R freeLMod I i I n Base R I R unitVec I i = j I R k I n k R k M j
197 8 196 sylanl1 R Field M Base I Mat R I curry M LIndF R freeLMod I i I n Base R I R unitVec I i = j I R k I n k R k M j
198 fveq1 n = f i n k = f i k
199 uncov i V k V i uncurry f k = f i k
200 199 el2v i uncurry f k = f i k
201 198 200 syl6eqr n = f i n k = i uncurry f k
202 201 oveq1d n = f i n k R k M j = i uncurry f k R k M j
203 202 mpteq2dv n = f i k I n k R k M j = k I i uncurry f k R k M j
204 203 oveq2d n = f i R k I n k R k M j = R k I i uncurry f k R k M j
205 204 mpteq2dv n = f i j I R k I n k R k M j = j I R k I i uncurry f k R k M j
206 205 eqeq2d n = f i R unitVec I i = j I R k I n k R k M j R unitVec I i = j I R k I i uncurry f k R k M j
207 206 ac6sfi I Fin i I n Base R I R unitVec I i = j I R k I n k R k M j f f : I Base R I i I R unitVec I i = j I R k I i uncurry f k R k M j
208 5 197 207 syl2anc R Field M Base I Mat R I curry M LIndF R freeLMod I f f : I Base R I i I R unitVec I i = j I R k I i uncurry f k R k M j
209 uncf f : I Base R I uncurry f : I × I Base R
210 13 14 frlmfibas R Field I × I Fin Base R I × I = Base R freeLMod I × I
211 12 210 sylan2 R Field I Fin Base R I × I = Base R freeLMod I × I
212 1 13 matbas I Fin R Field Base R freeLMod I × I = Base I Mat R
213 212 ancoms R Field I Fin Base R freeLMod I × I = Base I Mat R
214 211 213 eqtrd R Field I Fin Base R I × I = Base I Mat R
215 4 214 sylan2 R Field M Base I Mat R Base R I × I = Base I Mat R
216 215 eleq2d R Field M Base I Mat R uncurry f Base R I × I uncurry f Base I Mat R
217 elmapg Base R V I × I Fin uncurry f Base R I × I uncurry f : I × I Base R
218 22 23 217 sylancr M Base I Mat R uncurry f Base R I × I uncurry f : I × I Base R
219 218 adantl R Field M Base I Mat R uncurry f Base R I × I uncurry f : I × I Base R
220 216 219 bitr3d R Field M Base I Mat R uncurry f Base I Mat R uncurry f : I × I Base R
221 220 biimpar R Field M Base I Mat R uncurry f : I × I Base R uncurry f Base I Mat R
222 221 adantr R Field M Base I Mat R uncurry f : I × I Base R i I R unitVec I i = j I R k I i uncurry f k R k M j uncurry f Base I Mat R
223 nfv j R Field M Base I Mat R uncurry f : I × I Base R i I
224 nfmpt1 _ j j I R k I i uncurry f k R k M j
225 224 nfeq2 j R unitVec I i = j I R k I i uncurry f k R k M j
226 fveq1 R unitVec I i = j I R k I i uncurry f k R k M j R unitVec I i j = j I R k I i uncurry f k R k M j j
227 7 43 syl R Field R Ring
228 227 4 anim12i R Field M Base I Mat R R Ring I Fin
229 228 adantr R Field M Base I Mat R uncurry f : I × I Base R R Ring I Fin
230 equcom i = j j = i
231 ifbi i = j j = i if i = j 1 R 0 R = if j = i 1 R 0 R
232 230 231 ax-mp if i = j 1 R 0 R = if j = i 1 R 0 R
233 eqid 1 R = 1 R
234 eqid 0 R = 0 R
235 simpllr R Ring I Fin i I j I I Fin
236 simplll R Ring I Fin i I j I R Ring
237 simplr R Ring I Fin i I j I i I
238 simpr R Ring I Fin i I j I j I
239 eqid 1 I Mat R = 1 I Mat R
240 1 233 234 235 236 237 238 239 mat1ov R Ring I Fin i I j I i 1 I Mat R j = if i = j 1 R 0 R
241 df-3an R Ring I Fin i I R Ring I Fin i I
242 44 233 234 uvcvval R Ring I Fin i I j I R unitVec I i j = if j = i 1 R 0 R
243 241 242 sylanbr R Ring I Fin i I j I R unitVec I i j = if j = i 1 R 0 R
244 232 240 243 3eqtr4a R Ring I Fin i I j I i 1 I Mat R j = R unitVec I i j
245 229 244 sylanl1 R Field M Base I Mat R uncurry f : I × I Base R i I j I i 1 I Mat R j = R unitVec I i j
246 ovex R k I i uncurry f k R k M j V
247 eqid j I R k I i uncurry f k R k M j = j I R k I i uncurry f k R k M j
248 247 fvmpt2 j I R k I i uncurry f k R k M j V j I R k I i uncurry f k R k M j j = R k I i uncurry f k R k M j
249 246 248 mpan2 j I j I R k I i uncurry f k R k M j j = R k I i uncurry f k R k M j
250 249 adantl R Field M Base I Mat R uncurry f : I × I Base R i I j I j I R k I i uncurry f k R k M j j = R k I i uncurry f k R k M j
251 eqid R maMul I I I = R maMul I I I
252 simp-4l R Field M Base I Mat R uncurry f : I × I Base R i I j I R Field
253 4 ad4antlr R Field M Base I Mat R uncurry f : I × I Base R i I j I I Fin
254 218 biimpar M Base I Mat R uncurry f : I × I Base R uncurry f Base R I × I
255 254 ad5ant23 R Field M Base I Mat R uncurry f : I × I Base R i I j I uncurry f Base R I × I
256 simpr R Field M Base I Mat R M Base I Mat R
257 256 215 eleqtrrd R Field M Base I Mat R M Base R I × I
258 257 ad3antrrr R Field M Base I Mat R uncurry f : I × I Base R i I j I M Base R I × I
259 simplr R Field M Base I Mat R uncurry f : I × I Base R i I j I i I
260 simpr R Field M Base I Mat R uncurry f : I × I Base R i I j I j I
261 251 14 121 252 253 253 253 255 258 259 260 mamufv R Field M Base I Mat R uncurry f : I × I Base R i I j I i uncurry f R maMul I I I M j = R k I i uncurry f k R k M j
262 1 251 matmulr I Fin R Field R maMul I I I = I Mat R
263 262 ancoms R Field I Fin R maMul I I I = I Mat R
264 263 oveqd R Field I Fin uncurry f R maMul I I I M = uncurry f I Mat R M
265 264 oveqd R Field I Fin i uncurry f R maMul I I I M j = i uncurry f I Mat R M j
266 4 265 sylan2 R Field M Base I Mat R i uncurry f R maMul I I I M j = i uncurry f I Mat R M j
267 266 ad3antrrr R Field M Base I Mat R uncurry f : I × I Base R i I j I i uncurry f R maMul I I I M j = i uncurry f I Mat R M j
268 250 261 267 3eqtr2rd R Field M Base I Mat R uncurry f : I × I Base R i I j I i uncurry f I Mat R M j = j I R k I i uncurry f k R k M j j
269 245 268 eqeq12d R Field M Base I Mat R uncurry f : I × I Base R i I j I i 1 I Mat R j = i uncurry f I Mat R M j R unitVec I i j = j I R k I i uncurry f k R k M j j
270 226 269 syl5ibr R Field M Base I Mat R uncurry f : I × I Base R i I j I R unitVec I i = j I R k I i uncurry f k R k M j i 1 I Mat R j = i uncurry f I Mat R M j
271 270 ex R Field M Base I Mat R uncurry f : I × I Base R i I j I R unitVec I i = j I R k I i uncurry f k R k M j i 1 I Mat R j = i uncurry f I Mat R M j
272 271 com23 R Field M Base I Mat R uncurry f : I × I Base R i I R unitVec I i = j I R k I i uncurry f k R k M j j I i 1 I Mat R j = i uncurry f I Mat R M j
273 223 225 272 ralrimd R Field M Base I Mat R uncurry f : I × I Base R i I R unitVec I i = j I R k I i uncurry f k R k M j j I i 1 I Mat R j = i uncurry f I Mat R M j
274 273 ralimdva R Field M Base I Mat R uncurry f : I × I Base R i I R unitVec I i = j I R k I i uncurry f k R k M j i I j I i 1 I Mat R j = i uncurry f I Mat R M j
275 1 2 239 mat1bas R Ring I Fin 1 I Mat R Base I Mat R
276 13 14 frlmfibas R Ring I × I Fin Base R I × I = Base R freeLMod I × I
277 12 276 sylan2 R Ring I Fin Base R I × I = Base R freeLMod I × I
278 1 13 matbas I Fin R Ring Base R freeLMod I × I = Base I Mat R
279 278 ancoms R Ring I Fin Base R freeLMod I × I = Base I Mat R
280 277 279 eqtrd R Ring I Fin Base R I × I = Base I Mat R
281 275 280 eleqtrrd R Ring I Fin 1 I Mat R Base R I × I
282 elmapfn 1 I Mat R Base R I × I 1 I Mat R Fn I × I
283 281 282 syl R Ring I Fin 1 I Mat R Fn I × I
284 227 4 283 syl2an R Field M Base I Mat R 1 I Mat R Fn I × I
285 284 adantr R Field M Base I Mat R uncurry f : I × I Base R 1 I Mat R Fn I × I
286 1 matring I Fin R Ring I Mat R Ring
287 4 227 286 syl2anr R Field M Base I Mat R I Mat R Ring
288 287 adantr R Field M Base I Mat R uncurry f : I × I Base R I Mat R Ring
289 simplr R Field M Base I Mat R uncurry f : I × I Base R M Base I Mat R
290 eqid I Mat R = I Mat R
291 2 290 ringcl I Mat R Ring uncurry f Base I Mat R M Base I Mat R uncurry f I Mat R M Base I Mat R
292 288 221 289 291 syl3anc R Field M Base I Mat R uncurry f : I × I Base R uncurry f I Mat R M Base I Mat R
293 215 adantr R Field M Base I Mat R uncurry f : I × I Base R Base R I × I = Base I Mat R
294 292 293 eleqtrrd R Field M Base I Mat R uncurry f : I × I Base R uncurry f I Mat R M Base R I × I
295 elmapfn uncurry f I Mat R M Base R I × I uncurry f I Mat R M Fn I × I
296 294 295 syl R Field M Base I Mat R uncurry f : I × I Base R uncurry f I Mat R M Fn I × I
297 eqfnov2 1 I Mat R Fn I × I uncurry f I Mat R M Fn I × I 1 I Mat R = uncurry f I Mat R M i I j I i 1 I Mat R j = i uncurry f I Mat R M j
298 285 296 297 syl2anc R Field M Base I Mat R uncurry f : I × I Base R 1 I Mat R = uncurry f I Mat R M i I j I i 1 I Mat R j = i uncurry f I Mat R M j
299 274 298 sylibrd R Field M Base I Mat R uncurry f : I × I Base R i I R unitVec I i = j I R k I i uncurry f k R k M j 1 I Mat R = uncurry f I Mat R M
300 299 imp R Field M Base I Mat R uncurry f : I × I Base R i I R unitVec I i = j I R k I i uncurry f k R k M j 1 I Mat R = uncurry f I Mat R M
301 300 eqcomd R Field M Base I Mat R uncurry f : I × I Base R i I R unitVec I i = j I R k I i uncurry f k R k M j uncurry f I Mat R M = 1 I Mat R
302 oveq1 n = uncurry f n I Mat R M = uncurry f I Mat R M
303 302 eqeq1d n = uncurry f n I Mat R M = 1 I Mat R uncurry f I Mat R M = 1 I Mat R
304 303 rspcev uncurry f Base I Mat R uncurry f I Mat R M = 1 I Mat R n Base I Mat R n I Mat R M = 1 I Mat R
305 222 301 304 syl2anc R Field M Base I Mat R uncurry f : I × I Base R i I R unitVec I i = j I R k I i uncurry f k R k M j n Base I Mat R n I Mat R M = 1 I Mat R
306 305 expl R Field M Base I Mat R uncurry f : I × I Base R i I R unitVec I i = j I R k I i uncurry f k R k M j n Base I Mat R n I Mat R M = 1 I Mat R
307 209 306 sylani R Field M Base I Mat R f : I Base R I i I R unitVec I i = j I R k I i uncurry f k R k M j n Base I Mat R n I Mat R M = 1 I Mat R
308 307 exlimdv R Field M Base I Mat R f f : I Base R I i I R unitVec I i = j I R k I i uncurry f k R k M j n Base I Mat R n I Mat R M = 1 I Mat R
309 308 imp R Field M Base I Mat R f f : I Base R I i I R unitVec I i = j I R k I i uncurry f k R k M j n Base I Mat R n I Mat R M = 1 I Mat R
310 309 adantlr R Field M Base I Mat R I f f : I Base R I i I R unitVec I i = j I R k I i uncurry f k R k M j n Base I Mat R n I Mat R M = 1 I Mat R
311 208 310 syldan R Field M Base I Mat R I curry M LIndF R freeLMod I n Base I Mat R n I Mat R M = 1 I Mat R
312 6 simprbi R Field R CRing
313 eqid I maDet R = I maDet R
314 313 1 2 14 mdetcl R CRing M Base I Mat R I maDet R M Base R
315 313 1 2 14 mdetcl R CRing n Base I Mat R I maDet R n Base R
316 eqid r R = r R
317 14 316 121 dvdsrmul I maDet R M Base R I maDet R n Base R I maDet R M r R I maDet R n R I maDet R M
318 314 315 317 syl2an R CRing M Base I Mat R R CRing n Base I Mat R I maDet R M r R I maDet R n R I maDet R M
319 318 anandis R CRing M Base I Mat R n Base I Mat R I maDet R M r R I maDet R n R I maDet R M
320 319 anassrs R CRing M Base I Mat R n Base I Mat R I maDet R M r R I maDet R n R I maDet R M
321 320 adantrr R CRing M Base I Mat R n Base I Mat R n I Mat R M = 1 I Mat R I maDet R M r R I maDet R n R I maDet R M
322 fveq2 n I Mat R M = 1 I Mat R I maDet R n I Mat R M = I maDet R 1 I Mat R
323 1 2 313 121 290 mdetmul R CRing n Base I Mat R M Base I Mat R I maDet R n I Mat R M = I maDet R n R I maDet R M
324 323 3expa R CRing n Base I Mat R M Base I Mat R I maDet R n I Mat R M = I maDet R n R I maDet R M
325 324 an32s R CRing M Base I Mat R n Base I Mat R I maDet R n I Mat R M = I maDet R n R I maDet R M
326 313 1 239 233 mdet1 R CRing I Fin I maDet R 1 I Mat R = 1 R
327 4 326 sylan2 R CRing M Base I Mat R I maDet R 1 I Mat R = 1 R
328 327 adantr R CRing M Base I Mat R n Base I Mat R I maDet R 1 I Mat R = 1 R
329 325 328 eqeq12d R CRing M Base I Mat R n Base I Mat R I maDet R n I Mat R M = I maDet R 1 I Mat R I maDet R n R I maDet R M = 1 R
330 322 329 syl5ib R CRing M Base I Mat R n Base I Mat R n I Mat R M = 1 I Mat R I maDet R n R I maDet R M = 1 R
331 330 impr R CRing M Base I Mat R n Base I Mat R n I Mat R M = 1 I Mat R I maDet R n R I maDet R M = 1 R
332 331 breq2d R CRing M Base I Mat R n Base I Mat R n I Mat R M = 1 I Mat R I maDet R M r R I maDet R n R I maDet R M I maDet R M r R 1 R
333 eqid Unit R = Unit R
334 333 233 316 crngunit R CRing I maDet R M Unit R I maDet R M r R 1 R
335 334 ad2antrr R CRing M Base I Mat R n Base I Mat R n I Mat R M = 1 I Mat R I maDet R M Unit R I maDet R M r R 1 R
336 332 335 bitr4d R CRing M Base I Mat R n Base I Mat R n I Mat R M = 1 I Mat R I maDet R M r R I maDet R n R I maDet R M I maDet R M Unit R
337 321 336 mpbid R CRing M Base I Mat R n Base I Mat R n I Mat R M = 1 I Mat R I maDet R M Unit R
338 312 337 sylanl1 R Field M Base I Mat R n Base I Mat R n I Mat R M = 1 I Mat R I maDet R M Unit R
339 338 ad4ant14 R Field M Base I Mat R I curry M LIndF R freeLMod I n Base I Mat R n I Mat R M = 1 I Mat R I maDet R M Unit R
340 311 339 rexlimddv R Field M Base I Mat R I curry M LIndF R freeLMod I I maDet R M Unit R