Metamath Proof Explorer


Theorem matunitlindflem2

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

Ref Expression
Assertion matunitlindflem2 RFieldMBaseIMatRIcurryMLIndFRfreeLModIImaDetRMUnitR

Proof

Step Hyp Ref Expression
1 eqid IMatR=IMatR
2 eqid BaseIMatR=BaseIMatR
3 1 2 matrcl MBaseIMatRIFinRV
4 3 simpld MBaseIMatRIFin
5 4 ad3antlr RFieldMBaseIMatRIcurryMLIndFRfreeLModIIFin
6 isfld RFieldRDivRingRCRing
7 6 simplbi RFieldRDivRing
8 7 anim1i RFieldMBaseIMatRRDivRingMBaseIMatR
9 4 ad2antrl RDivRingMBaseIMatRIIFin
10 simpr RDivRingMBaseIMatRMBaseIMatR
11 xpfi IFinIFinI×IFin
12 11 anidms IFinI×IFin
13 eqid RfreeLModI×I=RfreeLModI×I
14 eqid BaseR=BaseR
15 13 14 frlmfibas RDivRingI×IFinBaseRI×I=BaseRfreeLModI×I
16 12 15 sylan2 RDivRingIFinBaseRI×I=BaseRfreeLModI×I
17 1 13 matbas IFinRDivRingBaseRfreeLModI×I=BaseIMatR
18 17 ancoms RDivRingIFinBaseRfreeLModI×I=BaseIMatR
19 16 18 eqtrd RDivRingIFinBaseRI×I=BaseIMatR
20 19 eleq2d RDivRingIFinMBaseRI×IMBaseIMatR
21 4 20 sylan2 RDivRingMBaseIMatRMBaseRI×IMBaseIMatR
22 fvex BaseRV
23 4 4 11 syl2anc MBaseIMatRI×IFin
24 elmapg BaseRVI×IFinMBaseRI×IM:I×IBaseR
25 22 23 24 sylancr MBaseIMatRMBaseRI×IM:I×IBaseR
26 25 adantl RDivRingMBaseIMatRMBaseRI×IM:I×IBaseR
27 21 26 bitr3d RDivRingMBaseIMatRMBaseIMatRM:I×IBaseR
28 10 27 mpbid RDivRingMBaseIMatRM:I×IBaseR
29 28 adantrr RDivRingMBaseIMatRIM:I×IBaseR
30 eldifsn IFinIFinI
31 30 biimpri IFinIIFin
32 4 31 sylan MBaseIMatRIIFin
33 32 adantl RDivRingMBaseIMatRIIFin
34 curf M:I×IBaseRIFinBaseRVcurryM:IBaseRI
35 22 34 mp3an3 M:I×IBaseRIFincurryM:IBaseRI
36 29 33 35 syl2anc RDivRingMBaseIMatRIcurryM:IBaseRI
37 9 36 jca RDivRingMBaseIMatRIIFincurryM:IBaseRI
38 37 ex RDivRingMBaseIMatRIIFincurryM:IBaseRI
39 38 imdistani RDivRingMBaseIMatRIRDivRingIFincurryM:IBaseRI
40 39 anassrs RDivRingMBaseIMatRIRDivRingIFincurryM:IBaseRI
41 anass RDivRingIFincurryM:IBaseRIRDivRingIFincurryM:IBaseRI
42 40 41 sylibr RDivRingMBaseIMatRIRDivRingIFincurryM:IBaseRI
43 drngring RDivRingRRing
44 eqid RunitVecI=RunitVecI
45 eqid RfreeLModI=RfreeLModI
46 eqid BaseRfreeLModI=BaseRfreeLModI
47 44 45 46 uvcff RRingIFinRunitVecI:IBaseRfreeLModI
48 43 47 sylan RDivRingIFinRunitVecI:IBaseRfreeLModI
49 48 ffvelrnda RDivRingIFiniIRunitVecIiBaseRfreeLModI
50 49 ad4ant14 RDivRingIFincurryM:IBaseRIcurryMLIndFRfreeLModIiIRunitVecIiBaseRfreeLModI
51 ffn curryM:IBaseRIcurryMFnI
52 fnima curryMFnIcurryMI=rancurryM
53 51 52 syl curryM:IBaseRIcurryMI=rancurryM
54 53 adantl RDivRingIFincurryM:IBaseRIcurryMI=rancurryM
55 54 fveq2d RDivRingIFincurryM:IBaseRILSpanRfreeLModIcurryMI=LSpanRfreeLModIrancurryM
56 55 adantr RDivRingIFincurryM:IBaseRIcurryMLIndFRfreeLModILSpanRfreeLModIcurryMI=LSpanRfreeLModIrancurryM
57 simplll RDivRingIFincurryM:IBaseRIcurryMLIndFRfreeLModIRDivRing
58 simpllr RDivRingIFincurryM:IBaseRIcurryMLIndFRfreeLModIIFin
59 45 frlmlmod RRingIFinRfreeLModILMod
60 43 59 sylan RDivRingIFinRfreeLModILMod
61 60 adantr RDivRingIFincurryM:IBaseRIRfreeLModILMod
62 lindfrn RfreeLModILModcurryMLIndFRfreeLModIrancurryMLIndSRfreeLModI
63 61 62 sylan RDivRingIFincurryM:IBaseRIcurryMLIndFRfreeLModIrancurryMLIndSRfreeLModI
64 45 frlmsca RDivRingIFinR=ScalarRfreeLModI
65 drngnzr RDivRingRNzRing
66 65 adantr RDivRingIFinRNzRing
67 64 66 eqeltrrd RDivRingIFinScalarRfreeLModINzRing
68 60 67 jca RDivRingIFinRfreeLModILModScalarRfreeLModINzRing
69 eqid ScalarRfreeLModI=ScalarRfreeLModI
70 46 69 lindff1 RfreeLModILModScalarRfreeLModINzRingcurryMLIndFRfreeLModIcurryM:domcurryM1-1BaseRfreeLModI
71 70 3expa RfreeLModILModScalarRfreeLModINzRingcurryMLIndFRfreeLModIcurryM:domcurryM1-1BaseRfreeLModI
72 68 71 sylan RDivRingIFincurryMLIndFRfreeLModIcurryM:domcurryM1-1BaseRfreeLModI
73 fdm curryM:IBaseRIdomcurryM=I
74 f1eq2 domcurryM=IcurryM:domcurryM1-1BaseRfreeLModIcurryM:I1-1BaseRfreeLModI
75 74 biimpac curryM:domcurryM1-1BaseRfreeLModIdomcurryM=IcurryM:I1-1BaseRfreeLModI
76 72 73 75 syl2an RDivRingIFincurryMLIndFRfreeLModIcurryM:IBaseRIcurryM:I1-1BaseRfreeLModI
77 76 an32s RDivRingIFincurryM:IBaseRIcurryMLIndFRfreeLModIcurryM:I1-1BaseRfreeLModI
78 f1f1orn curryM:I1-1BaseRfreeLModIcurryM:I1-1 ontorancurryM
79 77 78 syl RDivRingIFincurryM:IBaseRIcurryMLIndFRfreeLModIcurryM:I1-1 ontorancurryM
80 f1oeng IFincurryM:I1-1 ontorancurryMIrancurryM
81 58 79 80 syl2anc RDivRingIFincurryM:IBaseRIcurryMLIndFRfreeLModIIrancurryM
82 81 ensymd RDivRingIFincurryM:IBaseRIcurryMLIndFRfreeLModIrancurryMI
83 lindsenlbs RDivRingIFinrancurryMLIndSRfreeLModIrancurryMIrancurryMLBasisRfreeLModI
84 57 58 63 82 83 syl31anc RDivRingIFincurryM:IBaseRIcurryMLIndFRfreeLModIrancurryMLBasisRfreeLModI
85 eqid LBasisRfreeLModI=LBasisRfreeLModI
86 eqid LSpanRfreeLModI=LSpanRfreeLModI
87 46 85 86 lbssp rancurryMLBasisRfreeLModILSpanRfreeLModIrancurryM=BaseRfreeLModI
88 84 87 syl RDivRingIFincurryM:IBaseRIcurryMLIndFRfreeLModILSpanRfreeLModIrancurryM=BaseRfreeLModI
89 56 88 eqtrd RDivRingIFincurryM:IBaseRIcurryMLIndFRfreeLModILSpanRfreeLModIcurryMI=BaseRfreeLModI
90 89 adantr RDivRingIFincurryM:IBaseRIcurryMLIndFRfreeLModIiILSpanRfreeLModIcurryMI=BaseRfreeLModI
91 50 90 eleqtrrd RDivRingIFincurryM:IBaseRIcurryMLIndFRfreeLModIiIRunitVecIiLSpanRfreeLModIcurryMI
92 eqid BaseScalarRfreeLModI=BaseScalarRfreeLModI
93 eqid 0ScalarRfreeLModI=0ScalarRfreeLModI
94 eqid RfreeLModI=RfreeLModI
95 45 14 frlmfibas RRingIFinBaseRI=BaseRfreeLModI
96 95 feq3d RRingIFincurryM:IBaseRIcurryM:IBaseRfreeLModI
97 96 biimpa RRingIFincurryM:IBaseRIcurryM:IBaseRfreeLModI
98 59 adantr RRingIFincurryM:IBaseRIRfreeLModILMod
99 simplr RRingIFincurryM:IBaseRIIFin
100 86 46 92 69 93 94 97 98 99 elfilspd RRingIFincurryM:IBaseRIRunitVecIiLSpanRfreeLModIcurryMInBaseScalarRfreeLModIIRunitVecIi=RfreeLModInRfreeLModIfcurryM
101 45 frlmsca RRingIFinR=ScalarRfreeLModI
102 101 fveq2d RRingIFinBaseR=BaseScalarRfreeLModI
103 102 oveq1d RRingIFinBaseRI=BaseScalarRfreeLModII
104 103 adantr RRingIFincurryM:IBaseRIBaseRI=BaseScalarRfreeLModII
105 elmapi nBaseRIn:IBaseR
106 ffn n:IBaseRnFnI
107 106 adantl RRingIFincurryM:IBaseRIn:IBaseRnFnI
108 51 ad2antlr RRingIFincurryM:IBaseRIn:IBaseRcurryMFnI
109 simpllr RRingIFincurryM:IBaseRIn:IBaseRIFin
110 inidm II=I
111 eqidd RRingIFincurryM:IBaseRIn:IBaseRkInk=nk
112 eqidd RRingIFincurryM:IBaseRIn:IBaseRkIcurryMk=curryMk
113 107 108 109 109 110 111 112 offval RRingIFincurryM:IBaseRIn:IBaseRnRfreeLModIfcurryM=kInkRfreeLModIcurryMk
114 simp-4r RRingIFincurryM:IBaseRIn:IBaseRkIIFin
115 ffvelrn n:IBaseRkInkBaseR
116 115 adantll RRingIFincurryM:IBaseRIn:IBaseRkInkBaseR
117 ffvelrn curryM:IBaseRIkIcurryMkBaseRI
118 117 ad4ant24 RRingIFincurryM:IBaseRIn:IBaseRkIcurryMkBaseRI
119 95 ad3antrrr RRingIFincurryM:IBaseRIn:IBaseRkIBaseRI=BaseRfreeLModI
120 118 119 eleqtrd RRingIFincurryM:IBaseRIn:IBaseRkIcurryMkBaseRfreeLModI
121 eqid R=R
122 45 46 14 114 116 120 94 121 frlmvscafval RRingIFincurryM:IBaseRIn:IBaseRkInkRfreeLModIcurryMk=I×nkRfcurryMk
123 fvex nkV
124 fnconstg nkVI×nkFnI
125 123 124 mp1i RRingIFincurryM:IBaseRIn:IBaseRkII×nkFnI
126 elmapfn curryMkBaseRIcurryMkFnI
127 117 126 syl curryM:IBaseRIkIcurryMkFnI
128 127 ad4ant24 RRingIFincurryM:IBaseRIn:IBaseRkIcurryMkFnI
129 123 fvconst2 jII×nkj=nk
130 129 adantl RRingIFincurryM:IBaseRIn:IBaseRkIjII×nkj=nk
131 eqidd RRingIFincurryM:IBaseRIn:IBaseRkIjIcurryMkj=curryMkj
132 125 128 114 114 110 130 131 offval RRingIFincurryM:IBaseRIn:IBaseRkII×nkRfcurryMk=jInkRcurryMkj
133 122 132 eqtrd RRingIFincurryM:IBaseRIn:IBaseRkInkRfreeLModIcurryMk=jInkRcurryMkj
134 133 mpteq2dva RRingIFincurryM:IBaseRIn:IBaseRkInkRfreeLModIcurryMk=kIjInkRcurryMkj
135 113 134 eqtrd RRingIFincurryM:IBaseRIn:IBaseRnRfreeLModIfcurryM=kIjInkRcurryMkj
136 135 oveq2d RRingIFincurryM:IBaseRIn:IBaseRRfreeLModInRfreeLModIfcurryM=RfreeLModIkIjInkRcurryMkj
137 eqid 0RfreeLModI=0RfreeLModI
138 simplll RRingIFincurryM:IBaseRIn:IBaseRRRing
139 simp-5l RRingIFincurryM:IBaseRIn:IBaseRkIjIRRing
140 115 ad4ant23 RRingIFincurryM:IBaseRIn:IBaseRkIjInkBaseR
141 simplr RRingIFincurryM:IBaseRIn:IBaseRcurryM:IBaseRI
142 elmapi curryMkBaseRIcurryMk:IBaseR
143 117 142 syl curryM:IBaseRIkIcurryMk:IBaseR
144 143 ffvelrnda curryM:IBaseRIkIjIcurryMkjBaseR
145 141 144 sylanl1 RRingIFincurryM:IBaseRIn:IBaseRkIjIcurryMkjBaseR
146 14 121 ringcl RRingnkBaseRcurryMkjBaseRnkRcurryMkjBaseR
147 139 140 145 146 syl3anc RRingIFincurryM:IBaseRIn:IBaseRkIjInkRcurryMkjBaseR
148 147 fmpttd RRingIFincurryM:IBaseRIn:IBaseRkIjInkRcurryMkj:IBaseR
149 elmapg BaseRVIFinjInkRcurryMkjBaseRIjInkRcurryMkj:IBaseR
150 22 149 mpan IFinjInkRcurryMkjBaseRIjInkRcurryMkj:IBaseR
151 150 adantl RRingIFinjInkRcurryMkjBaseRIjInkRcurryMkj:IBaseR
152 95 eleq2d RRingIFinjInkRcurryMkjBaseRIjInkRcurryMkjBaseRfreeLModI
153 151 152 bitr3d RRingIFinjInkRcurryMkj:IBaseRjInkRcurryMkjBaseRfreeLModI
154 153 ad3antrrr RRingIFincurryM:IBaseRIn:IBaseRkIjInkRcurryMkj:IBaseRjInkRcurryMkjBaseRfreeLModI
155 148 154 mpbid RRingIFincurryM:IBaseRIn:IBaseRkIjInkRcurryMkjBaseRfreeLModI
156 mptexg IFinjInkRcurryMkjV
157 156 ralrimivw IFinkIjInkRcurryMkjV
158 eqid kIjInkRcurryMkj=kIjInkRcurryMkj
159 158 fnmpt kIjInkRcurryMkjVkIjInkRcurryMkjFnI
160 157 159 syl IFinkIjInkRcurryMkjFnI
161 id IFinIFin
162 fvexd IFin0RfreeLModIV
163 160 161 162 fndmfifsupp IFinfinSupp0RfreeLModIkIjInkRcurryMkj
164 163 ad3antlr RRingIFincurryM:IBaseRIn:IBaseRfinSupp0RfreeLModIkIjInkRcurryMkj
165 45 46 137 109 109 138 155 164 frlmgsum RRingIFincurryM:IBaseRIn:IBaseRRfreeLModIkIjInkRcurryMkj=jIRkInkRcurryMkj
166 136 165 eqtr2d RRingIFincurryM:IBaseRIn:IBaseRjIRkInkRcurryMkj=RfreeLModInRfreeLModIfcurryM
167 105 166 sylan2 RRingIFincurryM:IBaseRInBaseRIjIRkInkRcurryMkj=RfreeLModInRfreeLModIfcurryM
168 167 eqeq2d RRingIFincurryM:IBaseRInBaseRIRunitVecIi=jIRkInkRcurryMkjRunitVecIi=RfreeLModInRfreeLModIfcurryM
169 104 168 rexeqbidva RRingIFincurryM:IBaseRInBaseRIRunitVecIi=jIRkInkRcurryMkjnBaseScalarRfreeLModIIRunitVecIi=RfreeLModInRfreeLModIfcurryM
170 100 169 bitr4d RRingIFincurryM:IBaseRIRunitVecIiLSpanRfreeLModIcurryMInBaseRIRunitVecIi=jIRkInkRcurryMkj
171 43 170 sylanl1 RDivRingIFincurryM:IBaseRIRunitVecIiLSpanRfreeLModIcurryMInBaseRIRunitVecIi=jIRkInkRcurryMkj
172 171 ad2antrr RDivRingIFincurryM:IBaseRIcurryMLIndFRfreeLModIiIRunitVecIiLSpanRfreeLModIcurryMInBaseRIRunitVecIi=jIRkInkRcurryMkj
173 91 172 mpbid RDivRingIFincurryM:IBaseRIcurryMLIndFRfreeLModIiInBaseRIRunitVecIi=jIRkInkRcurryMkj
174 173 ralrimiva RDivRingIFincurryM:IBaseRIcurryMLIndFRfreeLModIiInBaseRIRunitVecIi=jIRkInkRcurryMkj
175 42 174 sylan RDivRingMBaseIMatRIcurryMLIndFRfreeLModIiInBaseRIRunitVecIi=jIRkInkRcurryMkj
176 10 21 mpbird RDivRingMBaseIMatRMBaseRI×I
177 elmapfn MBaseRI×IMFnI×I
178 176 177 syl RDivRingMBaseIMatRMFnI×I
179 4 adantl RDivRingMBaseIMatRIFin
180 an32 MFnI×IjIkIMFnI×IkIjI
181 df-3an MFnI×IkIjIMFnI×IkIjI
182 180 181 bitr4i MFnI×IjIkIMFnI×IkIjI
183 curfv MFnI×IkIjIIFincurryMkj=kMj
184 182 183 sylanb MFnI×IjIkIIFincurryMkj=kMj
185 184 an32s MFnI×IjIIFinkIcurryMkj=kMj
186 185 oveq2d MFnI×IjIIFinkInkRcurryMkj=nkRkMj
187 186 mpteq2dva MFnI×IjIIFinkInkRcurryMkj=kInkRkMj
188 187 an32s MFnI×IIFinjIkInkRcurryMkj=kInkRkMj
189 188 oveq2d MFnI×IIFinjIRkInkRcurryMkj=RkInkRkMj
190 189 mpteq2dva MFnI×IIFinjIRkInkRcurryMkj=jIRkInkRkMj
191 190 eqeq2d MFnI×IIFinRunitVecIi=jIRkInkRcurryMkjRunitVecIi=jIRkInkRkMj
192 191 rexbidv MFnI×IIFinnBaseRIRunitVecIi=jIRkInkRcurryMkjnBaseRIRunitVecIi=jIRkInkRkMj
193 192 ralbidv MFnI×IIFiniInBaseRIRunitVecIi=jIRkInkRcurryMkjiInBaseRIRunitVecIi=jIRkInkRkMj
194 178 179 193 syl2anc RDivRingMBaseIMatRiInBaseRIRunitVecIi=jIRkInkRcurryMkjiInBaseRIRunitVecIi=jIRkInkRkMj
195 194 ad2antrr RDivRingMBaseIMatRIcurryMLIndFRfreeLModIiInBaseRIRunitVecIi=jIRkInkRcurryMkjiInBaseRIRunitVecIi=jIRkInkRkMj
196 175 195 mpbid RDivRingMBaseIMatRIcurryMLIndFRfreeLModIiInBaseRIRunitVecIi=jIRkInkRkMj
197 8 196 sylanl1 RFieldMBaseIMatRIcurryMLIndFRfreeLModIiInBaseRIRunitVecIi=jIRkInkRkMj
198 fveq1 n=fink=fik
199 uncov iVkViuncurryfk=fik
200 199 el2v iuncurryfk=fik
201 198 200 eqtr4di n=fink=iuncurryfk
202 201 oveq1d n=finkRkMj=iuncurryfkRkMj
203 202 mpteq2dv n=fikInkRkMj=kIiuncurryfkRkMj
204 203 oveq2d n=fiRkInkRkMj=RkIiuncurryfkRkMj
205 204 mpteq2dv n=fijIRkInkRkMj=jIRkIiuncurryfkRkMj
206 205 eqeq2d n=fiRunitVecIi=jIRkInkRkMjRunitVecIi=jIRkIiuncurryfkRkMj
207 206 ac6sfi IFiniInBaseRIRunitVecIi=jIRkInkRkMjff:IBaseRIiIRunitVecIi=jIRkIiuncurryfkRkMj
208 5 197 207 syl2anc RFieldMBaseIMatRIcurryMLIndFRfreeLModIff:IBaseRIiIRunitVecIi=jIRkIiuncurryfkRkMj
209 uncf f:IBaseRIuncurryf:I×IBaseR
210 13 14 frlmfibas RFieldI×IFinBaseRI×I=BaseRfreeLModI×I
211 12 210 sylan2 RFieldIFinBaseRI×I=BaseRfreeLModI×I
212 1 13 matbas IFinRFieldBaseRfreeLModI×I=BaseIMatR
213 212 ancoms RFieldIFinBaseRfreeLModI×I=BaseIMatR
214 211 213 eqtrd RFieldIFinBaseRI×I=BaseIMatR
215 4 214 sylan2 RFieldMBaseIMatRBaseRI×I=BaseIMatR
216 215 eleq2d RFieldMBaseIMatRuncurryfBaseRI×IuncurryfBaseIMatR
217 elmapg BaseRVI×IFinuncurryfBaseRI×Iuncurryf:I×IBaseR
218 22 23 217 sylancr MBaseIMatRuncurryfBaseRI×Iuncurryf:I×IBaseR
219 218 adantl RFieldMBaseIMatRuncurryfBaseRI×Iuncurryf:I×IBaseR
220 216 219 bitr3d RFieldMBaseIMatRuncurryfBaseIMatRuncurryf:I×IBaseR
221 220 biimpar RFieldMBaseIMatRuncurryf:I×IBaseRuncurryfBaseIMatR
222 221 adantr RFieldMBaseIMatRuncurryf:I×IBaseRiIRunitVecIi=jIRkIiuncurryfkRkMjuncurryfBaseIMatR
223 nfv jRFieldMBaseIMatRuncurryf:I×IBaseRiI
224 nfmpt1 _jjIRkIiuncurryfkRkMj
225 224 nfeq2 jRunitVecIi=jIRkIiuncurryfkRkMj
226 fveq1 RunitVecIi=jIRkIiuncurryfkRkMjRunitVecIij=jIRkIiuncurryfkRkMjj
227 7 43 syl RFieldRRing
228 227 4 anim12i RFieldMBaseIMatRRRingIFin
229 228 adantr RFieldMBaseIMatRuncurryf:I×IBaseRRRingIFin
230 equcom i=jj=i
231 ifbi i=jj=iifi=j1R0R=ifj=i1R0R
232 230 231 ax-mp ifi=j1R0R=ifj=i1R0R
233 eqid 1R=1R
234 eqid 0R=0R
235 simpllr RRingIFiniIjIIFin
236 simplll RRingIFiniIjIRRing
237 simplr RRingIFiniIjIiI
238 simpr RRingIFiniIjIjI
239 eqid 1IMatR=1IMatR
240 1 233 234 235 236 237 238 239 mat1ov RRingIFiniIjIi1IMatRj=ifi=j1R0R
241 df-3an RRingIFiniIRRingIFiniI
242 44 233 234 uvcvval RRingIFiniIjIRunitVecIij=ifj=i1R0R
243 241 242 sylanbr RRingIFiniIjIRunitVecIij=ifj=i1R0R
244 232 240 243 3eqtr4a RRingIFiniIjIi1IMatRj=RunitVecIij
245 229 244 sylanl1 RFieldMBaseIMatRuncurryf:I×IBaseRiIjIi1IMatRj=RunitVecIij
246 ovex RkIiuncurryfkRkMjV
247 eqid jIRkIiuncurryfkRkMj=jIRkIiuncurryfkRkMj
248 247 fvmpt2 jIRkIiuncurryfkRkMjVjIRkIiuncurryfkRkMjj=RkIiuncurryfkRkMj
249 246 248 mpan2 jIjIRkIiuncurryfkRkMjj=RkIiuncurryfkRkMj
250 249 adantl RFieldMBaseIMatRuncurryf:I×IBaseRiIjIjIRkIiuncurryfkRkMjj=RkIiuncurryfkRkMj
251 eqid RmaMulIII=RmaMulIII
252 simp-4l RFieldMBaseIMatRuncurryf:I×IBaseRiIjIRField
253 4 ad4antlr RFieldMBaseIMatRuncurryf:I×IBaseRiIjIIFin
254 218 biimpar MBaseIMatRuncurryf:I×IBaseRuncurryfBaseRI×I
255 254 ad5ant23 RFieldMBaseIMatRuncurryf:I×IBaseRiIjIuncurryfBaseRI×I
256 simpr RFieldMBaseIMatRMBaseIMatR
257 256 215 eleqtrrd RFieldMBaseIMatRMBaseRI×I
258 257 ad3antrrr RFieldMBaseIMatRuncurryf:I×IBaseRiIjIMBaseRI×I
259 simplr RFieldMBaseIMatRuncurryf:I×IBaseRiIjIiI
260 simpr RFieldMBaseIMatRuncurryf:I×IBaseRiIjIjI
261 251 14 121 252 253 253 253 255 258 259 260 mamufv RFieldMBaseIMatRuncurryf:I×IBaseRiIjIiuncurryfRmaMulIIIMj=RkIiuncurryfkRkMj
262 1 251 matmulr IFinRFieldRmaMulIII=IMatR
263 262 ancoms RFieldIFinRmaMulIII=IMatR
264 263 oveqd RFieldIFinuncurryfRmaMulIIIM=uncurryfIMatRM
265 264 oveqd RFieldIFiniuncurryfRmaMulIIIMj=iuncurryfIMatRMj
266 4 265 sylan2 RFieldMBaseIMatRiuncurryfRmaMulIIIMj=iuncurryfIMatRMj
267 266 ad3antrrr RFieldMBaseIMatRuncurryf:I×IBaseRiIjIiuncurryfRmaMulIIIMj=iuncurryfIMatRMj
268 250 261 267 3eqtr2rd RFieldMBaseIMatRuncurryf:I×IBaseRiIjIiuncurryfIMatRMj=jIRkIiuncurryfkRkMjj
269 245 268 eqeq12d RFieldMBaseIMatRuncurryf:I×IBaseRiIjIi1IMatRj=iuncurryfIMatRMjRunitVecIij=jIRkIiuncurryfkRkMjj
270 226 269 syl5ibr RFieldMBaseIMatRuncurryf:I×IBaseRiIjIRunitVecIi=jIRkIiuncurryfkRkMji1IMatRj=iuncurryfIMatRMj
271 270 ex RFieldMBaseIMatRuncurryf:I×IBaseRiIjIRunitVecIi=jIRkIiuncurryfkRkMji1IMatRj=iuncurryfIMatRMj
272 271 com23 RFieldMBaseIMatRuncurryf:I×IBaseRiIRunitVecIi=jIRkIiuncurryfkRkMjjIi1IMatRj=iuncurryfIMatRMj
273 223 225 272 ralrimd RFieldMBaseIMatRuncurryf:I×IBaseRiIRunitVecIi=jIRkIiuncurryfkRkMjjIi1IMatRj=iuncurryfIMatRMj
274 273 ralimdva RFieldMBaseIMatRuncurryf:I×IBaseRiIRunitVecIi=jIRkIiuncurryfkRkMjiIjIi1IMatRj=iuncurryfIMatRMj
275 1 2 239 mat1bas RRingIFin1IMatRBaseIMatR
276 13 14 frlmfibas RRingI×IFinBaseRI×I=BaseRfreeLModI×I
277 12 276 sylan2 RRingIFinBaseRI×I=BaseRfreeLModI×I
278 1 13 matbas IFinRRingBaseRfreeLModI×I=BaseIMatR
279 278 ancoms RRingIFinBaseRfreeLModI×I=BaseIMatR
280 277 279 eqtrd RRingIFinBaseRI×I=BaseIMatR
281 275 280 eleqtrrd RRingIFin1IMatRBaseRI×I
282 elmapfn 1IMatRBaseRI×I1IMatRFnI×I
283 281 282 syl RRingIFin1IMatRFnI×I
284 227 4 283 syl2an RFieldMBaseIMatR1IMatRFnI×I
285 284 adantr RFieldMBaseIMatRuncurryf:I×IBaseR1IMatRFnI×I
286 1 matring IFinRRingIMatRRing
287 4 227 286 syl2anr RFieldMBaseIMatRIMatRRing
288 287 adantr RFieldMBaseIMatRuncurryf:I×IBaseRIMatRRing
289 simplr RFieldMBaseIMatRuncurryf:I×IBaseRMBaseIMatR
290 eqid IMatR=IMatR
291 2 290 ringcl IMatRRinguncurryfBaseIMatRMBaseIMatRuncurryfIMatRMBaseIMatR
292 288 221 289 291 syl3anc RFieldMBaseIMatRuncurryf:I×IBaseRuncurryfIMatRMBaseIMatR
293 215 adantr RFieldMBaseIMatRuncurryf:I×IBaseRBaseRI×I=BaseIMatR
294 292 293 eleqtrrd RFieldMBaseIMatRuncurryf:I×IBaseRuncurryfIMatRMBaseRI×I
295 elmapfn uncurryfIMatRMBaseRI×IuncurryfIMatRMFnI×I
296 294 295 syl RFieldMBaseIMatRuncurryf:I×IBaseRuncurryfIMatRMFnI×I
297 eqfnov2 1IMatRFnI×IuncurryfIMatRMFnI×I1IMatR=uncurryfIMatRMiIjIi1IMatRj=iuncurryfIMatRMj
298 285 296 297 syl2anc RFieldMBaseIMatRuncurryf:I×IBaseR1IMatR=uncurryfIMatRMiIjIi1IMatRj=iuncurryfIMatRMj
299 274 298 sylibrd RFieldMBaseIMatRuncurryf:I×IBaseRiIRunitVecIi=jIRkIiuncurryfkRkMj1IMatR=uncurryfIMatRM
300 299 imp RFieldMBaseIMatRuncurryf:I×IBaseRiIRunitVecIi=jIRkIiuncurryfkRkMj1IMatR=uncurryfIMatRM
301 300 eqcomd RFieldMBaseIMatRuncurryf:I×IBaseRiIRunitVecIi=jIRkIiuncurryfkRkMjuncurryfIMatRM=1IMatR
302 oveq1 n=uncurryfnIMatRM=uncurryfIMatRM
303 302 eqeq1d n=uncurryfnIMatRM=1IMatRuncurryfIMatRM=1IMatR
304 303 rspcev uncurryfBaseIMatRuncurryfIMatRM=1IMatRnBaseIMatRnIMatRM=1IMatR
305 222 301 304 syl2anc RFieldMBaseIMatRuncurryf:I×IBaseRiIRunitVecIi=jIRkIiuncurryfkRkMjnBaseIMatRnIMatRM=1IMatR
306 305 expl RFieldMBaseIMatRuncurryf:I×IBaseRiIRunitVecIi=jIRkIiuncurryfkRkMjnBaseIMatRnIMatRM=1IMatR
307 209 306 sylani RFieldMBaseIMatRf:IBaseRIiIRunitVecIi=jIRkIiuncurryfkRkMjnBaseIMatRnIMatRM=1IMatR
308 307 exlimdv RFieldMBaseIMatRff:IBaseRIiIRunitVecIi=jIRkIiuncurryfkRkMjnBaseIMatRnIMatRM=1IMatR
309 308 imp RFieldMBaseIMatRff:IBaseRIiIRunitVecIi=jIRkIiuncurryfkRkMjnBaseIMatRnIMatRM=1IMatR
310 309 adantlr RFieldMBaseIMatRIff:IBaseRIiIRunitVecIi=jIRkIiuncurryfkRkMjnBaseIMatRnIMatRM=1IMatR
311 208 310 syldan RFieldMBaseIMatRIcurryMLIndFRfreeLModInBaseIMatRnIMatRM=1IMatR
312 6 simprbi RFieldRCRing
313 eqid ImaDetR=ImaDetR
314 313 1 2 14 mdetcl RCRingMBaseIMatRImaDetRMBaseR
315 313 1 2 14 mdetcl RCRingnBaseIMatRImaDetRnBaseR
316 eqid rR=rR
317 14 316 121 dvdsrmul ImaDetRMBaseRImaDetRnBaseRImaDetRMrRImaDetRnRImaDetRM
318 314 315 317 syl2an RCRingMBaseIMatRRCRingnBaseIMatRImaDetRMrRImaDetRnRImaDetRM
319 318 anandis RCRingMBaseIMatRnBaseIMatRImaDetRMrRImaDetRnRImaDetRM
320 319 anassrs RCRingMBaseIMatRnBaseIMatRImaDetRMrRImaDetRnRImaDetRM
321 320 adantrr RCRingMBaseIMatRnBaseIMatRnIMatRM=1IMatRImaDetRMrRImaDetRnRImaDetRM
322 fveq2 nIMatRM=1IMatRImaDetRnIMatRM=ImaDetR1IMatR
323 1 2 313 121 290 mdetmul RCRingnBaseIMatRMBaseIMatRImaDetRnIMatRM=ImaDetRnRImaDetRM
324 323 3expa RCRingnBaseIMatRMBaseIMatRImaDetRnIMatRM=ImaDetRnRImaDetRM
325 324 an32s RCRingMBaseIMatRnBaseIMatRImaDetRnIMatRM=ImaDetRnRImaDetRM
326 313 1 239 233 mdet1 RCRingIFinImaDetR1IMatR=1R
327 4 326 sylan2 RCRingMBaseIMatRImaDetR1IMatR=1R
328 327 adantr RCRingMBaseIMatRnBaseIMatRImaDetR1IMatR=1R
329 325 328 eqeq12d RCRingMBaseIMatRnBaseIMatRImaDetRnIMatRM=ImaDetR1IMatRImaDetRnRImaDetRM=1R
330 322 329 syl5ib RCRingMBaseIMatRnBaseIMatRnIMatRM=1IMatRImaDetRnRImaDetRM=1R
331 330 impr RCRingMBaseIMatRnBaseIMatRnIMatRM=1IMatRImaDetRnRImaDetRM=1R
332 331 breq2d RCRingMBaseIMatRnBaseIMatRnIMatRM=1IMatRImaDetRMrRImaDetRnRImaDetRMImaDetRMrR1R
333 eqid UnitR=UnitR
334 333 233 316 crngunit RCRingImaDetRMUnitRImaDetRMrR1R
335 334 ad2antrr RCRingMBaseIMatRnBaseIMatRnIMatRM=1IMatRImaDetRMUnitRImaDetRMrR1R
336 332 335 bitr4d RCRingMBaseIMatRnBaseIMatRnIMatRM=1IMatRImaDetRMrRImaDetRnRImaDetRMImaDetRMUnitR
337 321 336 mpbid RCRingMBaseIMatRnBaseIMatRnIMatRM=1IMatRImaDetRMUnitR
338 312 337 sylanl1 RFieldMBaseIMatRnBaseIMatRnIMatRM=1IMatRImaDetRMUnitR
339 338 ad4ant14 RFieldMBaseIMatRIcurryMLIndFRfreeLModInBaseIMatRnIMatRM=1IMatRImaDetRMUnitR
340 311 339 rexlimddv RFieldMBaseIMatRIcurryMLIndFRfreeLModIImaDetRMUnitR