Metamath Proof Explorer

Theorem matunitlindflem2

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

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