Metamath Proof Explorer

Theorem matunitlindflem1

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

Ref Expression
Assertion matunitlindflem1 
|- ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) -> ( -. curry M LIndF ( R freeLMod I ) -> ( ( I maDet R ) ` M ) = ( 0g ` R ) ) )

Proof

Step Hyp Ref Expression
1 isfld 
 |-  ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) )
2 1 simplbi 
 |-  ( R e. Field -> R e. DivRing )
3 drngring 
 |-  ( R e. DivRing -> R e. Ring )
4 2 3 syl 
 |-  ( R e. Field -> R e. Ring )
5 eqid 
 |-  ( R freeLMod I ) = ( R freeLMod I )
6 5 frlmlmod 
 |-  ( ( R e. Ring /\ I e. ( Fin \ { (/) } ) ) -> ( R freeLMod I ) e. LMod )
7 6 adantlr 
 |-  ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) -> ( R freeLMod I ) e. LMod )
8 simpr 
 |-  ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) -> I e. ( Fin \ { (/) } ) )
9 eldifi 
 |-  ( I e. ( Fin \ { (/) } ) -> I e. Fin )
10 eqid 
 |-  ( Base ` R ) = ( Base ` R )
11 5 10 frlmfibas 
 |-  ( ( R e. Ring /\ I e. Fin ) -> ( ( Base ` R ) ^m I ) = ( Base ` ( R freeLMod I ) ) )
12 9 11 sylan2 
 |-  ( ( R e. Ring /\ I e. ( Fin \ { (/) } ) ) -> ( ( Base ` R ) ^m I ) = ( Base ` ( R freeLMod I ) ) )
13 fvex 
 |-  ( Base ` R ) e. _V
14 curf 
 |-  ( ( M : ( I X. I ) --> ( Base ` R ) /\ I e. ( Fin \ { (/) } ) /\ ( Base ` R ) e. _V ) -> curry M : I --> ( ( Base ` R ) ^m I ) )
15 13 14 mp3an3 
 |-  ( ( M : ( I X. I ) --> ( Base ` R ) /\ I e. ( Fin \ { (/) } ) ) -> curry M : I --> ( ( Base ` R ) ^m I ) )
16 feq3 
 |-  ( ( ( Base ` R ) ^m I ) = ( Base ` ( R freeLMod I ) ) -> ( curry M : I --> ( ( Base ` R ) ^m I ) <-> curry M : I --> ( Base ` ( R freeLMod I ) ) ) )
17 16 biimpa 
 |-  ( ( ( ( Base ` R ) ^m I ) = ( Base ` ( R freeLMod I ) ) /\ curry M : I --> ( ( Base ` R ) ^m I ) ) -> curry M : I --> ( Base ` ( R freeLMod I ) ) )
18 12 15 17 syl2an 
 |-  ( ( ( R e. Ring /\ I e. ( Fin \ { (/) } ) ) /\ ( M : ( I X. I ) --> ( Base ` R ) /\ I e. ( Fin \ { (/) } ) ) ) -> curry M : I --> ( Base ` ( R freeLMod I ) ) )
19 18 anandirs 
 |-  ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) -> curry M : I --> ( Base ` ( R freeLMod I ) ) )
20 eqid 
 |-  ( Base ` ( R freeLMod I ) ) = ( Base ` ( R freeLMod I ) )
21 eqid 
 |-  ( Scalar ` ( R freeLMod I ) ) = ( Scalar ` ( R freeLMod I ) )
22 eqid 
 |-  ( .s ` ( R freeLMod I ) ) = ( .s ` ( R freeLMod I ) )
23 eqid 
 |-  ( 0g ` ( R freeLMod I ) ) = ( 0g ` ( R freeLMod I ) )
24 eqid 
 |-  ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) = ( 0g ` ( Scalar ` ( R freeLMod I ) ) )
25 eqid 
 |-  ( Base ` ( ( Scalar ` ( R freeLMod I ) ) freeLMod I ) ) = ( Base ` ( ( Scalar ` ( R freeLMod I ) ) freeLMod I ) )
26 20 21 22 23 24 25 islindf4 
 |-  ( ( ( R freeLMod I ) e. LMod /\ I e. ( Fin \ { (/) } ) /\ curry M : I --> ( Base ` ( R freeLMod I ) ) ) -> ( curry M LIndF ( R freeLMod I ) <-> A. f e. ( Base ` ( ( Scalar ` ( R freeLMod I ) ) freeLMod I ) ) ( ( ( R freeLMod I ) gsum ( f oF ( .s ` ( R freeLMod I ) ) curry M ) ) = ( 0g ` ( R freeLMod I ) ) -> f = ( I X. { ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) } ) ) ) )
27 7 8 19 26 syl3anc 
 |-  ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) -> ( curry M LIndF ( R freeLMod I ) <-> A. f e. ( Base ` ( ( Scalar ` ( R freeLMod I ) ) freeLMod I ) ) ( ( ( R freeLMod I ) gsum ( f oF ( .s ` ( R freeLMod I ) ) curry M ) ) = ( 0g ` ( R freeLMod I ) ) -> f = ( I X. { ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) } ) ) ) )
28 5 frlmsca 
 |-  ( ( R e. Ring /\ I e. ( Fin \ { (/) } ) ) -> R = ( Scalar ` ( R freeLMod I ) ) )
29 28 fvoveq1d 
 |-  ( ( R e. Ring /\ I e. ( Fin \ { (/) } ) ) -> ( Base ` ( R freeLMod I ) ) = ( Base ` ( ( Scalar ` ( R freeLMod I ) ) freeLMod I ) ) )
30 12 29 eqtrd 
 |-  ( ( R e. Ring /\ I e. ( Fin \ { (/) } ) ) -> ( ( Base ` R ) ^m I ) = ( Base ` ( ( Scalar ` ( R freeLMod I ) ) freeLMod I ) ) )
31 30 adantlr 
 |-  ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) -> ( ( Base ` R ) ^m I ) = ( Base ` ( ( Scalar ` ( R freeLMod I ) ) freeLMod I ) ) )
32 elmapi 
 |-  ( f e. ( ( Base ` R ) ^m I ) -> f : I --> ( Base ` R ) )
33 ffn 
 |-  ( f : I --> ( Base ` R ) -> f Fn I )
34 33 adantl 
 |-  ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) -> f Fn I )
35 19 ffnd 
 |-  ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) -> curry M Fn I )
36 35 adantr 
 |-  ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) -> curry M Fn I )
37 simplr 
 |-  ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) -> I e. ( Fin \ { (/) } ) )
38 inidm 
 |-  ( I i^i I ) = I
39 eqidd 
 |-  ( ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) /\ n e. I ) -> ( f ` n ) = ( f ` n ) )
40 eqidd 
 |-  ( ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) /\ n e. I ) -> ( curry M ` n ) = ( curry M ` n ) )
41 34 36 37 37 38 39 40 offval 
 |-  ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) -> ( f oF ( .s ` ( R freeLMod I ) ) curry M ) = ( n e. I |-> ( ( f ` n ) ( .s ` ( R freeLMod I ) ) ( curry M ` n ) ) ) )
42 simpllr 
 |-  ( ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) /\ n e. I ) -> I e. ( Fin \ { (/) } ) )
43 ffvelcdm 
 |-  ( ( f : I --> ( Base ` R ) /\ n e. I ) -> ( f ` n ) e. ( Base ` R ) )
44 43 adantll 
 |-  ( ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) /\ n e. I ) -> ( f ` n ) e. ( Base ` R ) )
45 19 ffvelcdmda 
 |-  ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ n e. I ) -> ( curry M ` n ) e. ( Base ` ( R freeLMod I ) ) )
46 45 adantlr 
 |-  ( ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) /\ n e. I ) -> ( curry M ` n ) e. ( Base ` ( R freeLMod I ) ) )
47 eqid 
 |-  ( .r ` R ) = ( .r ` R )
48 5 20 10 42 44 46 22 47 frlmvscafval 
 |-  ( ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) /\ n e. I ) -> ( ( f ` n ) ( .s ` ( R freeLMod I ) ) ( curry M ` n ) ) = ( ( I X. { ( f ` n ) } ) oF ( .r ` R ) ( curry M ` n ) ) )
49 fvex 
 |-  ( f ` n ) e. _V
50 fnconstg 
 |-  ( ( f ` n ) e. _V -> ( I X. { ( f ` n ) } ) Fn I )
51 49 50 mp1i 
 |-  ( ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) /\ n e. I ) -> ( I X. { ( f ` n ) } ) Fn I )
52 15 ffvelcdmda 
 |-  ( ( ( M : ( I X. I ) --> ( Base ` R ) /\ I e. ( Fin \ { (/) } ) ) /\ n e. I ) -> ( curry M ` n ) e. ( ( Base ` R ) ^m I ) )
53 elmapfn 
 |-  ( ( curry M ` n ) e. ( ( Base ` R ) ^m I ) -> ( curry M ` n ) Fn I )
54 52 53 syl 
 |-  ( ( ( M : ( I X. I ) --> ( Base ` R ) /\ I e. ( Fin \ { (/) } ) ) /\ n e. I ) -> ( curry M ` n ) Fn I )
55 54 adantlll 
 |-  ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ n e. I ) -> ( curry M ` n ) Fn I )
56 55 adantlr 
 |-  ( ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) /\ n e. I ) -> ( curry M ` n ) Fn I )
57 49 fvconst2 
 |-  ( k e. I -> ( ( I X. { ( f ` n ) } ) ` k ) = ( f ` n ) )
58 57 adantl 
 |-  ( ( ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) /\ n e. I ) /\ k e. I ) -> ( ( I X. { ( f ` n ) } ) ` k ) = ( f ` n ) )
59 ffn 
 |-  ( M : ( I X. I ) --> ( Base ` R ) -> M Fn ( I X. I ) )
60 59 anim2i 
 |-  ( ( I e. ( Fin \ { (/) } ) /\ M : ( I X. I ) --> ( Base ` R ) ) -> ( I e. ( Fin \ { (/) } ) /\ M Fn ( I X. I ) ) )
61 60 ancoms 
 |-  ( ( M : ( I X. I ) --> ( Base ` R ) /\ I e. ( Fin \ { (/) } ) ) -> ( I e. ( Fin \ { (/) } ) /\ M Fn ( I X. I ) ) )
62 61 ad4ant23 
 |-  ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) -> ( I e. ( Fin \ { (/) } ) /\ M Fn ( I X. I ) ) )
63 curfv 
 |-  ( ( ( M Fn ( I X. I ) /\ n e. I /\ k e. I ) /\ I e. ( Fin \ { (/) } ) ) -> ( ( curry M ` n ) ` k ) = ( n M k ) )
64 63 3exp1 
 |-  ( M Fn ( I X. I ) -> ( n e. I -> ( k e. I -> ( I e. ( Fin \ { (/) } ) -> ( ( curry M ` n ) ` k ) = ( n M k ) ) ) ) )
65 64 com4r 
 |-  ( I e. ( Fin \ { (/) } ) -> ( M Fn ( I X. I ) -> ( n e. I -> ( k e. I -> ( ( curry M ` n ) ` k ) = ( n M k ) ) ) ) )
66 65 imp41 
 |-  ( ( ( ( I e. ( Fin \ { (/) } ) /\ M Fn ( I X. I ) ) /\ n e. I ) /\ k e. I ) -> ( ( curry M ` n ) ` k ) = ( n M k ) )
67 62 66 sylanl1 
 |-  ( ( ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) /\ n e. I ) /\ k e. I ) -> ( ( curry M ` n ) ` k ) = ( n M k ) )
68 51 56 42 42 38 58 67 offval 
 |-  ( ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) /\ n e. I ) -> ( ( I X. { ( f ` n ) } ) oF ( .r ` R ) ( curry M ` n ) ) = ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) )
69 48 68 eqtrd 
 |-  ( ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) /\ n e. I ) -> ( ( f ` n ) ( .s ` ( R freeLMod I ) ) ( curry M ` n ) ) = ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) )
70 69 mpteq2dva 
 |-  ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) -> ( n e. I |-> ( ( f ` n ) ( .s ` ( R freeLMod I ) ) ( curry M ` n ) ) ) = ( n e. I |-> ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) )
71 41 70 eqtrd 
 |-  ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) -> ( f oF ( .s ` ( R freeLMod I ) ) curry M ) = ( n e. I |-> ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) )
72 71 oveq2d 
 |-  ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) -> ( ( R freeLMod I ) gsum ( f oF ( .s ` ( R freeLMod I ) ) curry M ) ) = ( ( R freeLMod I ) gsum ( n e. I |-> ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) )
73 simplll 
 |-  ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) -> R e. Ring )
74 simp-4l 
 |-  ( ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ f : I --> ( Base ` R ) ) /\ n e. I ) /\ k e. I ) -> R e. Ring )
75 43 ad4ant23 
 |-  ( ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ f : I --> ( Base ` R ) ) /\ n e. I ) /\ k e. I ) -> ( f ` n ) e. ( Base ` R ) )
76 fovcdm 
 |-  ( ( M : ( I X. I ) --> ( Base ` R ) /\ n e. I /\ k e. I ) -> ( n M k ) e. ( Base ` R ) )
77 76 ad5ant245 
 |-  ( ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ f : I --> ( Base ` R ) ) /\ n e. I ) /\ k e. I ) -> ( n M k ) e. ( Base ` R ) )
78 10 47 ringcl 
 |-  ( ( R e. Ring /\ ( f ` n ) e. ( Base ` R ) /\ ( n M k ) e. ( Base ` R ) ) -> ( ( f ` n ) ( .r ` R ) ( n M k ) ) e. ( Base ` R ) )
79 74 75 77 78 syl3anc 
 |-  ( ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ f : I --> ( Base ` R ) ) /\ n e. I ) /\ k e. I ) -> ( ( f ` n ) ( .r ` R ) ( n M k ) ) e. ( Base ` R ) )
80 79 fmpttd 
 |-  ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ f : I --> ( Base ` R ) ) /\ n e. I ) -> ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) : I --> ( Base ` R ) )
81 80 adantllr 
 |-  ( ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) /\ n e. I ) -> ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) : I --> ( Base ` R ) )
82 elmapg 
 |-  ( ( ( Base ` R ) e. _V /\ I e. ( Fin \ { (/) } ) ) -> ( ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) e. ( ( Base ` R ) ^m I ) <-> ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) : I --> ( Base ` R ) ) )
83 13 82 mpan 
 |-  ( I e. ( Fin \ { (/) } ) -> ( ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) e. ( ( Base ` R ) ^m I ) <-> ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) : I --> ( Base ` R ) ) )
84 83 adantl 
 |-  ( ( R e. Ring /\ I e. ( Fin \ { (/) } ) ) -> ( ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) e. ( ( Base ` R ) ^m I ) <-> ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) : I --> ( Base ` R ) ) )
85 12 eleq2d 
 |-  ( ( R e. Ring /\ I e. ( Fin \ { (/) } ) ) -> ( ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) e. ( ( Base ` R ) ^m I ) <-> ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) e. ( Base ` ( R freeLMod I ) ) ) )
86 84 85 bitr3d 
 |-  ( ( R e. Ring /\ I e. ( Fin \ { (/) } ) ) -> ( ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) : I --> ( Base ` R ) <-> ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) e. ( Base ` ( R freeLMod I ) ) ) )
87 86 ad5ant13 
 |-  ( ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) /\ n e. I ) -> ( ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) : I --> ( Base ` R ) <-> ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) e. ( Base ` ( R freeLMod I ) ) ) )
88 81 87 mpbid 
 |-  ( ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) /\ n e. I ) -> ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) e. ( Base ` ( R freeLMod I ) ) )
89 mptexg 
 |-  ( I e. ( Fin \ { (/) } ) -> ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) e. _V )
90 89 ralrimivw 
 |-  ( I e. ( Fin \ { (/) } ) -> A. n e. I ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) e. _V )
91 eqid 
 |-  ( n e. I |-> ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) = ( n e. I |-> ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) )
92 91 fnmpt 
 |-  ( A. n e. I ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) e. _V -> ( n e. I |-> ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) Fn I )
93 90 92 syl 
 |-  ( I e. ( Fin \ { (/) } ) -> ( n e. I |-> ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) Fn I )
94 fvexd 
 |-  ( I e. ( Fin \ { (/) } ) -> ( 0g ` ( R freeLMod I ) ) e. _V )
95 93 9 94 fndmfifsupp 
 |-  ( I e. ( Fin \ { (/) } ) -> ( n e. I |-> ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) finSupp ( 0g ` ( R freeLMod I ) ) )
96 95 ad2antlr 
 |-  ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) -> ( n e. I |-> ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) finSupp ( 0g ` ( R freeLMod I ) ) )
97 5 20 23 37 37 73 88 96 frlmgsum 
 |-  ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) -> ( ( R freeLMod I ) gsum ( n e. I |-> ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( k e. I |-> ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) )
98 72 97 eqtr2d 
 |-  ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) -> ( k e. I |-> ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( ( R freeLMod I ) gsum ( f oF ( .s ` ( R freeLMod I ) ) curry M ) ) )
99 32 98 sylan2 
 |-  ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f e. ( ( Base ` R ) ^m I ) ) -> ( k e. I |-> ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( ( R freeLMod I ) gsum ( f oF ( .s ` ( R freeLMod I ) ) curry M ) ) )
100 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
101 5 100 frlm0 
 |-  ( ( R e. Ring /\ I e. ( Fin \ { (/) } ) ) -> ( I X. { ( 0g ` R ) } ) = ( 0g ` ( R freeLMod I ) ) )
102 101 ad4ant13 
 |-  ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f e. ( ( Base ` R ) ^m I ) ) -> ( I X. { ( 0g ` R ) } ) = ( 0g ` ( R freeLMod I ) ) )
103 99 102 eqeq12d 
 |-  ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f e. ( ( Base ` R ) ^m I ) ) -> ( ( k e. I |-> ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) <-> ( ( R freeLMod I ) gsum ( f oF ( .s ` ( R freeLMod I ) ) curry M ) ) = ( 0g ` ( R freeLMod I ) ) ) )
104 28 fveq2d 
 |-  ( ( R e. Ring /\ I e. ( Fin \ { (/) } ) ) -> ( 0g ` R ) = ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) )
105 104 sneqd 
 |-  ( ( R e. Ring /\ I e. ( Fin \ { (/) } ) ) -> { ( 0g ` R ) } = { ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) } )
106 105 xpeq2d 
 |-  ( ( R e. Ring /\ I e. ( Fin \ { (/) } ) ) -> ( I X. { ( 0g ` R ) } ) = ( I X. { ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) } ) )
107 106 eqeq2d 
 |-  ( ( R e. Ring /\ I e. ( Fin \ { (/) } ) ) -> ( f = ( I X. { ( 0g ` R ) } ) <-> f = ( I X. { ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) } ) ) )
108 107 ad4ant13 
 |-  ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f e. ( ( Base ` R ) ^m I ) ) -> ( f = ( I X. { ( 0g ` R ) } ) <-> f = ( I X. { ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) } ) ) )
109 103 108 imbi12d 
 |-  ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f e. ( ( Base ` R ) ^m I ) ) -> ( ( ( k e. I |-> ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) -> f = ( I X. { ( 0g ` R ) } ) ) <-> ( ( ( R freeLMod I ) gsum ( f oF ( .s ` ( R freeLMod I ) ) curry M ) ) = ( 0g ` ( R freeLMod I ) ) -> f = ( I X. { ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) } ) ) ) )
110 31 109 raleqbidva 
 |-  ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) -> ( A. f e. ( ( Base ` R ) ^m I ) ( ( k e. I |-> ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) -> f = ( I X. { ( 0g ` R ) } ) ) <-> A. f e. ( Base ` ( ( Scalar ` ( R freeLMod I ) ) freeLMod I ) ) ( ( ( R freeLMod I ) gsum ( f oF ( .s ` ( R freeLMod I ) ) curry M ) ) = ( 0g ` ( R freeLMod I ) ) -> f = ( I X. { ( 0g ` ( Scalar ` ( R freeLMod I ) ) ) } ) ) ) )
111 27 110 bitr4d 
 |-  ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) -> ( curry M LIndF ( R freeLMod I ) <-> A. f e. ( ( Base ` R ) ^m I ) ( ( k e. I |-> ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) -> f = ( I X. { ( 0g ` R ) } ) ) ) )
112 111 notbid 
 |-  ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) -> ( -. curry M LIndF ( R freeLMod I ) <-> -. A. f e. ( ( Base ` R ) ^m I ) ( ( k e. I |-> ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) -> f = ( I X. { ( 0g ` R ) } ) ) ) )
113 rexanali 
 |-  ( E. f e. ( ( Base ` R ) ^m I ) ( ( k e. I |-> ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) /\ -. f = ( I X. { ( 0g ` R ) } ) ) <-> -. A. f e. ( ( Base ` R ) ^m I ) ( ( k e. I |-> ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) -> f = ( I X. { ( 0g ` R ) } ) ) )
114 112 113 bitr4di 
 |-  ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) -> ( -. curry M LIndF ( R freeLMod I ) <-> E. f e. ( ( Base ` R ) ^m I ) ( ( k e. I |-> ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) /\ -. f = ( I X. { ( 0g ` R ) } ) ) ) )
115 4 114 sylanl1 
 |-  ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) -> ( -. curry M LIndF ( R freeLMod I ) <-> E. f e. ( ( Base ` R ) ^m I ) ( ( k e. I |-> ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) /\ -. f = ( I X. { ( 0g ` R ) } ) ) ) )
116 fconstfv 
 |-  ( f : I --> { ( 0g ` R ) } <-> ( f Fn I /\ A. i e. I ( f ` i ) = ( 0g ` R ) ) )
117 fvex 
 |-  ( 0g ` R ) e. _V
118 117 fconst2 
 |-  ( f : I --> { ( 0g ` R ) } <-> f = ( I X. { ( 0g ` R ) } ) )
119 116 118 sylbb1 
 |-  ( ( f Fn I /\ A. i e. I ( f ` i ) = ( 0g ` R ) ) -> f = ( I X. { ( 0g ` R ) } ) )
120 119 ex 
 |-  ( f Fn I -> ( A. i e. I ( f ` i ) = ( 0g ` R ) -> f = ( I X. { ( 0g ` R ) } ) ) )
121 120 con3d 
 |-  ( f Fn I -> ( -. f = ( I X. { ( 0g ` R ) } ) -> -. A. i e. I ( f ` i ) = ( 0g ` R ) ) )
122 df-ne 
 |-  ( ( f ` i ) =/= ( 0g ` R ) <-> -. ( f ` i ) = ( 0g ` R ) )
123 122 rexbii 
 |-  ( E. i e. I ( f ` i ) =/= ( 0g ` R ) <-> E. i e. I -. ( f ` i ) = ( 0g ` R ) )
124 rexnal 
 |-  ( E. i e. I -. ( f ` i ) = ( 0g ` R ) <-> -. A. i e. I ( f ` i ) = ( 0g ` R ) )
125 123 124 bitri 
 |-  ( E. i e. I ( f ` i ) =/= ( 0g ` R ) <-> -. A. i e. I ( f ` i ) = ( 0g ` R ) )
126 121 125 imbitrrdi 
 |-  ( f Fn I -> ( -. f = ( I X. { ( 0g ` R ) } ) -> E. i e. I ( f ` i ) =/= ( 0g ` R ) ) )
127 33 126 syl 
 |-  ( f : I --> ( Base ` R ) -> ( -. f = ( I X. { ( 0g ` R ) } ) -> E. i e. I ( f ` i ) =/= ( 0g ` R ) ) )
128 127 adantl 
 |-  ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) -> ( -. f = ( I X. { ( 0g ` R ) } ) -> E. i e. I ( f ` i ) =/= ( 0g ` R ) ) )
129 neldifsn 
 |-  -. i e. ( I \ { i } )
130 difss 
 |-  ( I \ { i } ) C_ I
131 diffi 
 |-  ( I e. Fin -> ( I \ { i } ) e. Fin )
132 131 ad4antlr 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( -. i e. ( I \ { i } ) /\ ( I \ { i } ) C_ I ) ) -> ( I \ { i } ) e. Fin )
133 eleq2 
 |-  ( y = (/) -> ( i e. y <-> i e. (/) ) )
134 133 notbid 
 |-  ( y = (/) -> ( -. i e. y <-> -. i e. (/) ) )
135 sseq1 
 |-  ( y = (/) -> ( y C_ I <-> (/) C_ I ) )
136 134 135 anbi12d 
 |-  ( y = (/) -> ( ( -. i e. y /\ y C_ I ) <-> ( -. i e. (/) /\ (/) C_ I ) ) )
137 136 anbi2d 
 |-  ( y = (/) -> ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( -. i e. y /\ y C_ I ) ) <-> ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( -. i e. (/) /\ (/) C_ I ) ) ) )
138 mpteq1 
 |-  ( y = (/) -> ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) = ( n e. (/) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) )
139 mpt0 
 |-  ( n e. (/) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) = (/)
140 138 139 eqtrdi 
 |-  ( y = (/) -> ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) = (/) )
141 140 oveq2d 
 |-  ( y = (/) -> ( R gsum ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( R gsum (/) ) )
142 100 gsum0 
 |-  ( R gsum (/) ) = ( 0g ` R )
143 141 142 eqtrdi 
 |-  ( y = (/) -> ( R gsum ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( 0g ` R ) )
144 143 oveq1d 
 |-  ( y = (/) -> ( ( R gsum ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) = ( ( 0g ` R ) ( +g ` R ) ( i M k ) ) )
145 144 ifeq1d 
 |-  ( y = (/) -> if ( j = i , ( ( R gsum ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) = if ( j = i , ( ( 0g ` R ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) )
146 145 mpoeq3dv 
 |-  ( y = (/) -> ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) = ( j e. I , k e. I |-> if ( j = i , ( ( 0g ` R ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) )
147 146 fveq2d 
 |-  ( y = (/) -> ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( 0g ` R ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) )
148 147 eqeq2d 
 |-  ( y = (/) -> ( ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) <-> ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( 0g ` R ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) ) )
149 137 148 imbi12d 
 |-  ( y = (/) -> ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( -. i e. y /\ y C_ I ) ) -> ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) ) <-> ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( -. i e. (/) /\ (/) C_ I ) ) -> ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( 0g ` R ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) ) ) )
150 elequ2 
 |-  ( y = x -> ( i e. y <-> i e. x ) )
151 150 notbid 
 |-  ( y = x -> ( -. i e. y <-> -. i e. x ) )
152 sseq1 
 |-  ( y = x -> ( y C_ I <-> x C_ I ) )
153 151 152 anbi12d 
 |-  ( y = x -> ( ( -. i e. y /\ y C_ I ) <-> ( -. i e. x /\ x C_ I ) ) )
154 153 anbi2d 
 |-  ( y = x -> ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( -. i e. y /\ y C_ I ) ) <-> ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( -. i e. x /\ x C_ I ) ) ) )
155 mpteq1 
 |-  ( y = x -> ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) = ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) )
156 155 oveq2d 
 |-  ( y = x -> ( R gsum ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) )
157 156 oveq1d 
 |-  ( y = x -> ( ( R gsum ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) = ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) )
158 157 ifeq1d 
 |-  ( y = x -> if ( j = i , ( ( R gsum ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) = if ( j = i , ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) )
159 158 mpoeq3dv 
 |-  ( y = x -> ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) = ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) )
160 159 fveq2d 
 |-  ( y = x -> ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) )
161 160 eqeq2d 
 |-  ( y = x -> ( ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) <-> ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) ) )
162 154 161 imbi12d 
 |-  ( y = x -> ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( -. i e. y /\ y C_ I ) ) -> ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) ) <-> ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( -. i e. x /\ x C_ I ) ) -> ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) ) ) )
163 eleq2 
 |-  ( y = ( x u. { z } ) -> ( i e. y <-> i e. ( x u. { z } ) ) )
164 163 notbid 
 |-  ( y = ( x u. { z } ) -> ( -. i e. y <-> -. i e. ( x u. { z } ) ) )
165 sseq1 
 |-  ( y = ( x u. { z } ) -> ( y C_ I <-> ( x u. { z } ) C_ I ) )
166 164 165 anbi12d 
 |-  ( y = ( x u. { z } ) -> ( ( -. i e. y /\ y C_ I ) <-> ( -. i e. ( x u. { z } ) /\ ( x u. { z } ) C_ I ) ) )
167 166 anbi2d 
 |-  ( y = ( x u. { z } ) -> ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( -. i e. y /\ y C_ I ) ) <-> ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( -. i e. ( x u. { z } ) /\ ( x u. { z } ) C_ I ) ) ) )
168 mpteq1 
 |-  ( y = ( x u. { z } ) -> ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) = ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) )
169 168 oveq2d 
 |-  ( y = ( x u. { z } ) -> ( R gsum ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( R gsum ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) )
170 169 oveq1d 
 |-  ( y = ( x u. { z } ) -> ( ( R gsum ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) = ( ( R gsum ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) )
171 170 ifeq1d 
 |-  ( y = ( x u. { z } ) -> if ( j = i , ( ( R gsum ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) = if ( j = i , ( ( R gsum ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) )
172 171 mpoeq3dv 
 |-  ( y = ( x u. { z } ) -> ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) = ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) )
173 172 fveq2d 
 |-  ( y = ( x u. { z } ) -> ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) )
174 173 eqeq2d 
 |-  ( y = ( x u. { z } ) -> ( ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) <-> ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) ) )
175 167 174 imbi12d 
 |-  ( y = ( x u. { z } ) -> ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( -. i e. y /\ y C_ I ) ) -> ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) ) <-> ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( -. i e. ( x u. { z } ) /\ ( x u. { z } ) C_ I ) ) -> ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) ) ) )
176 eleq2 
 |-  ( y = ( I \ { i } ) -> ( i e. y <-> i e. ( I \ { i } ) ) )
177 176 notbid 
 |-  ( y = ( I \ { i } ) -> ( -. i e. y <-> -. i e. ( I \ { i } ) ) )
178 sseq1 
 |-  ( y = ( I \ { i } ) -> ( y C_ I <-> ( I \ { i } ) C_ I ) )
179 177 178 anbi12d 
 |-  ( y = ( I \ { i } ) -> ( ( -. i e. y /\ y C_ I ) <-> ( -. i e. ( I \ { i } ) /\ ( I \ { i } ) C_ I ) ) )
180 179 anbi2d 
 |-  ( y = ( I \ { i } ) -> ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( -. i e. y /\ y C_ I ) ) <-> ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( -. i e. ( I \ { i } ) /\ ( I \ { i } ) C_ I ) ) ) )
181 mpteq1 
 |-  ( y = ( I \ { i } ) -> ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) = ( n e. ( I \ { i } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) )
182 181 oveq2d 
 |-  ( y = ( I \ { i } ) -> ( R gsum ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( R gsum ( n e. ( I \ { i } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) )
183 182 oveq1d 
 |-  ( y = ( I \ { i } ) -> ( ( R gsum ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) = ( ( R gsum ( n e. ( I \ { i } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) )
184 183 ifeq1d 
 |-  ( y = ( I \ { i } ) -> if ( j = i , ( ( R gsum ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) = if ( j = i , ( ( R gsum ( n e. ( I \ { i } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) )
185 184 mpoeq3dv 
 |-  ( y = ( I \ { i } ) -> ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) = ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. ( I \ { i } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) )
186 185 fveq2d 
 |-  ( y = ( I \ { i } ) -> ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. ( I \ { i } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) )
187 186 eqeq2d 
 |-  ( y = ( I \ { i } ) -> ( ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) <-> ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. ( I \ { i } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) ) )
188 180 187 imbi12d 
 |-  ( y = ( I \ { i } ) -> ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( -. i e. y /\ y C_ I ) ) -> ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) ) <-> ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( -. i e. ( I \ { i } ) /\ ( I \ { i } ) C_ I ) ) -> ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. ( I \ { i } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) ) ) )
189 fnov 
 |-  ( M Fn ( I X. I ) <-> M = ( j e. I , k e. I |-> ( j M k ) ) )
190 59 189 sylib 
 |-  ( M : ( I X. I ) --> ( Base ` R ) -> M = ( j e. I , k e. I |-> ( j M k ) ) )
191 190 adantl 
 |-  ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) -> M = ( j e. I , k e. I |-> ( j M k ) ) )
192 ringgrp 
 |-  ( R e. Ring -> R e. Grp )
193 4 192 syl 
 |-  ( R e. Field -> R e. Grp )
194 oveq1 
 |-  ( i = j -> ( i M k ) = ( j M k ) )
195 194 equcoms 
 |-  ( j = i -> ( i M k ) = ( j M k ) )
196 195 oveq2d 
 |-  ( j = i -> ( ( 0g ` R ) ( +g ` R ) ( i M k ) ) = ( ( 0g ` R ) ( +g ` R ) ( j M k ) ) )
197 simp1l 
 |-  ( ( ( R e. Grp /\ M : ( I X. I ) --> ( Base ` R ) ) /\ j e. I /\ k e. I ) -> R e. Grp )
198 fovcdm 
 |-  ( ( M : ( I X. I ) --> ( Base ` R ) /\ j e. I /\ k e. I ) -> ( j M k ) e. ( Base ` R ) )
199 198 3adant1l 
 |-  ( ( ( R e. Grp /\ M : ( I X. I ) --> ( Base ` R ) ) /\ j e. I /\ k e. I ) -> ( j M k ) e. ( Base ` R ) )
200 eqid 
 |-  ( +g ` R ) = ( +g ` R )
201 10 200 100 grplid 
 |-  ( ( R e. Grp /\ ( j M k ) e. ( Base ` R ) ) -> ( ( 0g ` R ) ( +g ` R ) ( j M k ) ) = ( j M k ) )
202 197 199 201 syl2anc 
 |-  ( ( ( R e. Grp /\ M : ( I X. I ) --> ( Base ` R ) ) /\ j e. I /\ k e. I ) -> ( ( 0g ` R ) ( +g ` R ) ( j M k ) ) = ( j M k ) )
203 196 202 sylan9eqr 
 |-  ( ( ( ( R e. Grp /\ M : ( I X. I ) --> ( Base ` R ) ) /\ j e. I /\ k e. I ) /\ j = i ) -> ( ( 0g ` R ) ( +g ` R ) ( i M k ) ) = ( j M k ) )
204 eqidd 
 |-  ( ( ( ( R e. Grp /\ M : ( I X. I ) --> ( Base ` R ) ) /\ j e. I /\ k e. I ) /\ -. j = i ) -> ( j M k ) = ( j M k ) )
205 203 204 ifeqda 
 |-  ( ( ( R e. Grp /\ M : ( I X. I ) --> ( Base ` R ) ) /\ j e. I /\ k e. I ) -> if ( j = i , ( ( 0g ` R ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) = ( j M k ) )
206 205 mpoeq3dva 
 |-  ( ( R e. Grp /\ M : ( I X. I ) --> ( Base ` R ) ) -> ( j e. I , k e. I |-> if ( j = i , ( ( 0g ` R ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) = ( j e. I , k e. I |-> ( j M k ) ) )
207 193 206 sylan 
 |-  ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) -> ( j e. I , k e. I |-> if ( j = i , ( ( 0g ` R ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) = ( j e. I , k e. I |-> ( j M k ) ) )
208 191 207 eqtr4d 
 |-  ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) -> M = ( j e. I , k e. I |-> if ( j = i , ( ( 0g ` R ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) )
209 208 fveq2d 
 |-  ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) -> ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( 0g ` R ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) )
210 209 ad4antr 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( -. i e. (/) /\ (/) C_ I ) ) -> ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( 0g ` R ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) )
211 elun1 
 |-  ( i e. x -> i e. ( x u. { z } ) )
212 211 con3i 
 |-  ( -. i e. ( x u. { z } ) -> -. i e. x )
213 ssun1 
 |-  x C_ ( x u. { z } )
214 sstr 
 |-  ( ( x C_ ( x u. { z } ) /\ ( x u. { z } ) C_ I ) -> x C_ I )
215 213 214 mpan 
 |-  ( ( x u. { z } ) C_ I -> x C_ I )
216 212 215 anim12i 
 |-  ( ( -. i e. ( x u. { z } ) /\ ( x u. { z } ) C_ I ) -> ( -. i e. x /\ x C_ I ) )
217 216 anim2i 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( -. i e. ( x u. { z } ) /\ ( x u. { z } ) C_ I ) ) -> ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( -. i e. x /\ x C_ I ) ) )
218 217 adantr 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( -. i e. ( x u. { z } ) /\ ( x u. { z } ) C_ I ) ) /\ -. z e. x ) -> ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( -. i e. x /\ x C_ I ) ) )
219 velsn 
 |-  ( i e. { z } <-> i = z )
220 elun2 
 |-  ( i e. { z } -> i e. ( x u. { z } ) )
221 219 220 sylbir 
 |-  ( i = z -> i e. ( x u. { z } ) )
222 221 necon3bi 
 |-  ( -. i e. ( x u. { z } ) -> i =/= z )
223 222 anim1i 
 |-  ( ( -. i e. ( x u. { z } ) /\ ( x u. { z } ) C_ I ) -> ( i =/= z /\ ( x u. { z } ) C_ I ) )
224 ringcmn 
 |-  ( R e. Ring -> R e. CMnd )
225 4 224 syl 
 |-  ( R e. Field -> R e. CMnd )
226 225 ad7antr 
 |-  ( ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) /\ -. z e. x ) /\ k e. I ) -> R e. CMnd )
227 simplr 
 |-  ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) -> I e. Fin )
228 215 adantl 
 |-  ( ( i =/= z /\ ( x u. { z } ) C_ I ) -> x C_ I )
229 ssfi 
 |-  ( ( I e. Fin /\ x C_ I ) -> x e. Fin )
230 227 228 229 syl2an 
 |-  ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) -> x e. Fin )
231 230 ad5ant13 
 |-  ( ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) /\ -. z e. x ) /\ k e. I ) -> x e. Fin )
232 215 sselda 
 |-  ( ( ( x u. { z } ) C_ I /\ n e. x ) -> n e. I )
233 232 adantll 
 |-  ( ( ( i =/= z /\ ( x u. { z } ) C_ I ) /\ n e. x ) -> n e. I )
234 233 ad4ant24 
 |-  ( ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) /\ k e. I ) /\ n e. x ) -> n e. I )
235 4 ad6antr 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ k e. I ) /\ n e. I ) -> R e. Ring )
236 2 ad2antrr 
 |-  ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) -> R e. DivRing )
237 ffvelcdm 
 |-  ( ( f : I --> ( Base ` R ) /\ i e. I ) -> ( f ` i ) e. ( Base ` R ) )
238 237 anim2i 
 |-  ( ( R e. DivRing /\ ( f : I --> ( Base ` R ) /\ i e. I ) ) -> ( R e. DivRing /\ ( f ` i ) e. ( Base ` R ) ) )
239 238 anassrs 
 |-  ( ( ( R e. DivRing /\ f : I --> ( Base ` R ) ) /\ i e. I ) -> ( R e. DivRing /\ ( f ` i ) e. ( Base ` R ) ) )
240 eqid 
 |-  ( invr ` R ) = ( invr ` R )
241 10 100 240 drnginvrcl 
 |-  ( ( R e. DivRing /\ ( f ` i ) e. ( Base ` R ) /\ ( f ` i ) =/= ( 0g ` R ) ) -> ( ( invr ` R ) ` ( f ` i ) ) e. ( Base ` R ) )
242 241 3expa 
 |-  ( ( ( R e. DivRing /\ ( f ` i ) e. ( Base ` R ) ) /\ ( f ` i ) =/= ( 0g ` R ) ) -> ( ( invr ` R ) ` ( f ` i ) ) e. ( Base ` R ) )
243 239 242 sylan 
 |-  ( ( ( ( R e. DivRing /\ f : I --> ( Base ` R ) ) /\ i e. I ) /\ ( f ` i ) =/= ( 0g ` R ) ) -> ( ( invr ` R ) ` ( f ` i ) ) e. ( Base ` R ) )
244 243 anasss 
 |-  ( ( ( R e. DivRing /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) -> ( ( invr ` R ) ` ( f ` i ) ) e. ( Base ` R ) )
245 236 244 sylanl1 
 |-  ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) -> ( ( invr ` R ) ` ( f ` i ) ) e. ( Base ` R ) )
246 245 ad2antrr 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ k e. I ) /\ n e. I ) -> ( ( invr ` R ) ` ( f ` i ) ) e. ( Base ` R ) )
247 43 ad5ant25 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ k e. I ) /\ n e. I ) -> ( f ` n ) e. ( Base ` R ) )
248 simp-4r 
 |-  ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) -> M : ( I X. I ) --> ( Base ` R ) )
249 76 3expa 
 |-  ( ( ( M : ( I X. I ) --> ( Base ` R ) /\ n e. I ) /\ k e. I ) -> ( n M k ) e. ( Base ` R ) )
250 249 an32s 
 |-  ( ( ( M : ( I X. I ) --> ( Base ` R ) /\ k e. I ) /\ n e. I ) -> ( n M k ) e. ( Base ` R ) )
251 248 250 sylanl1 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ k e. I ) /\ n e. I ) -> ( n M k ) e. ( Base ` R ) )
252 235 247 251 78 syl3anc 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ k e. I ) /\ n e. I ) -> ( ( f ` n ) ( .r ` R ) ( n M k ) ) e. ( Base ` R ) )
253 10 47 ringcl 
 |-  ( ( R e. Ring /\ ( ( invr ` R ) ` ( f ` i ) ) e. ( Base ` R ) /\ ( ( f ` n ) ( .r ` R ) ( n M k ) ) e. ( Base ` R ) ) -> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) e. ( Base ` R ) )
254 235 246 252 253 syl3anc 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ k e. I ) /\ n e. I ) -> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) e. ( Base ` R ) )
255 254 adantllr 
 |-  ( ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) /\ k e. I ) /\ n e. I ) -> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) e. ( Base ` R ) )
256 234 255 syldan 
 |-  ( ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) /\ k e. I ) /\ n e. x ) -> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) e. ( Base ` R ) )
257 256 adantllr 
 |-  ( ( ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) /\ -. z e. x ) /\ k e. I ) /\ n e. x ) -> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) e. ( Base ` R ) )
258 vex 
 |-  z e. _V
259 258 a1i 
 |-  ( ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) /\ -. z e. x ) /\ k e. I ) -> z e. _V )
260 simplr 
 |-  ( ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) /\ -. z e. x ) /\ k e. I ) -> -. z e. x )
261 ssun2 
 |-  { z } C_ ( x u. { z } )
262 sstr 
 |-  ( ( { z } C_ ( x u. { z } ) /\ ( x u. { z } ) C_ I ) -> { z } C_ I )
263 261 262 mpan 
 |-  ( ( x u. { z } ) C_ I -> { z } C_ I )
264 258 snss 
 |-  ( z e. I <-> { z } C_ I )
265 263 264 sylibr 
 |-  ( ( x u. { z } ) C_ I -> z e. I )
266 265 adantl 
 |-  ( ( i =/= z /\ ( x u. { z } ) C_ I ) -> z e. I )
267 4 ad6antr 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ z e. I ) /\ k e. I ) -> R e. Ring )
268 4 ad5antr 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ z e. I ) -> R e. Ring )
269 245 adantr 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ z e. I ) -> ( ( invr ` R ) ` ( f ` i ) ) e. ( Base ` R ) )
270 ffvelcdm 
 |-  ( ( f : I --> ( Base ` R ) /\ z e. I ) -> ( f ` z ) e. ( Base ` R ) )
271 270 ad4ant24 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ z e. I ) -> ( f ` z ) e. ( Base ` R ) )
272 10 47 ringcl 
 |-  ( ( R e. Ring /\ ( ( invr ` R ) ` ( f ` i ) ) e. ( Base ` R ) /\ ( f ` z ) e. ( Base ` R ) ) -> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` z ) ) e. ( Base ` R ) )
273 268 269 271 272 syl3anc 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ z e. I ) -> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` z ) ) e. ( Base ` R ) )
274 273 adantr 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ z e. I ) /\ k e. I ) -> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` z ) ) e. ( Base ` R ) )
275 fovcdm 
 |-  ( ( M : ( I X. I ) --> ( Base ` R ) /\ z e. I /\ k e. I ) -> ( z M k ) e. ( Base ` R ) )
276 275 3expa 
 |-  ( ( ( M : ( I X. I ) --> ( Base ` R ) /\ z e. I ) /\ k e. I ) -> ( z M k ) e. ( Base ` R ) )
277 248 276 sylanl1 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ z e. I ) /\ k e. I ) -> ( z M k ) e. ( Base ` R ) )
278 10 47 ringcl 
 |-  ( ( R e. Ring /\ ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` z ) ) e. ( Base ` R ) /\ ( z M k ) e. ( Base ` R ) ) -> ( ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` z ) ) ( .r ` R ) ( z M k ) ) e. ( Base ` R ) )
279 267 274 277 278 syl3anc 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ z e. I ) /\ k e. I ) -> ( ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` z ) ) ( .r ` R ) ( z M k ) ) e. ( Base ` R ) )
280 266 279 sylanl2 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) /\ k e. I ) -> ( ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` z ) ) ( .r ` R ) ( z M k ) ) e. ( Base ` R ) )
281 280 adantlr 
 |-  ( ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) /\ -. z e. x ) /\ k e. I ) -> ( ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` z ) ) ( .r ` R ) ( z M k ) ) e. ( Base ` R ) )
282 fveq2 
 |-  ( n = z -> ( f ` n ) = ( f ` z ) )
283 oveq1 
 |-  ( n = z -> ( n M k ) = ( z M k ) )
284 282 283 oveq12d 
 |-  ( n = z -> ( ( f ` n ) ( .r ` R ) ( n M k ) ) = ( ( f ` z ) ( .r ` R ) ( z M k ) ) )
285 284 oveq2d 
 |-  ( n = z -> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) = ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` z ) ( .r ` R ) ( z M k ) ) ) )
286 245 ad2antrr 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ z e. I ) /\ k e. I ) -> ( ( invr ` R ) ` ( f ` i ) ) e. ( Base ` R ) )
287 270 ad5ant24 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ z e. I ) /\ k e. I ) -> ( f ` z ) e. ( Base ` R ) )
288 10 47 ringass 
 |-  ( ( R e. Ring /\ ( ( ( invr ` R ) ` ( f ` i ) ) e. ( Base ` R ) /\ ( f ` z ) e. ( Base ` R ) /\ ( z M k ) e. ( Base ` R ) ) ) -> ( ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` z ) ) ( .r ` R ) ( z M k ) ) = ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` z ) ( .r ` R ) ( z M k ) ) ) )
289 267 286 287 277 288 syl13anc 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ z e. I ) /\ k e. I ) -> ( ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` z ) ) ( .r ` R ) ( z M k ) ) = ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` z ) ( .r ` R ) ( z M k ) ) ) )
290 289 eqcomd 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ z e. I ) /\ k e. I ) -> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` z ) ( .r ` R ) ( z M k ) ) ) = ( ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` z ) ) ( .r ` R ) ( z M k ) ) )
291 266 290 sylanl2 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) /\ k e. I ) -> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` z ) ( .r ` R ) ( z M k ) ) ) = ( ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` z ) ) ( .r ` R ) ( z M k ) ) )
292 285 291 sylan9eqr 
 |-  ( ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) /\ k e. I ) /\ n = z ) -> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) = ( ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` z ) ) ( .r ` R ) ( z M k ) ) )
293 292 adantllr 
 |-  ( ( ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) /\ -. z e. x ) /\ k e. I ) /\ n = z ) -> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) = ( ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` z ) ) ( .r ` R ) ( z M k ) ) )
294 10 200 226 231 257 259 260 281 293 gsumunsnd 
 |-  ( ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) /\ -. z e. x ) /\ k e. I ) -> ( R gsum ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` z ) ) ( .r ` R ) ( z M k ) ) ) )
295 294 oveq1d 
 |-  ( ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) /\ -. z e. x ) /\ k e. I ) -> ( ( R gsum ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) = ( ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` z ) ) ( .r ` R ) ( z M k ) ) ) ( +g ` R ) ( i M k ) ) )
296 ringabl 
 |-  ( R e. Ring -> R e. Abel )
297 4 296 syl 
 |-  ( R e. Field -> R e. Abel )
298 297 ad6antr 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( x u. { z } ) C_ I ) /\ k e. I ) -> R e. Abel )
299 225 ad6antr 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ x C_ I ) /\ k e. I ) -> R e. CMnd )
300 vex 
 |-  x e. _V
301 300 a1i 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ x C_ I ) /\ k e. I ) -> x e. _V )
302 ssel2 
 |-  ( ( x C_ I /\ n e. x ) -> n e. I )
303 302 254 sylan2 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ k e. I ) /\ ( x C_ I /\ n e. x ) ) -> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) e. ( Base ` R ) )
304 303 anassrs 
 |-  ( ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ k e. I ) /\ x C_ I ) /\ n e. x ) -> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) e. ( Base ` R ) )
305 304 fmpttd 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ k e. I ) /\ x C_ I ) -> ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) : x --> ( Base ` R ) )
306 305 an32s 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ x C_ I ) /\ k e. I ) -> ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) : x --> ( Base ` R ) )
307 ovex 
 |-  ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) e. _V
308 eqid 
 |-  ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) = ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) )
309 307 308 fnmpti 
 |-  ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) Fn x
310 309 a1i 
 |-  ( ( I e. Fin /\ x C_ I ) -> ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) Fn x )
311 fvexd 
 |-  ( ( I e. Fin /\ x C_ I ) -> ( 0g ` R ) e. _V )
312 310 229 311 fndmfifsupp 
 |-  ( ( I e. Fin /\ x C_ I ) -> ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) finSupp ( 0g ` R ) )
313 312 adantll 
 |-  ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ x C_ I ) -> ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) finSupp ( 0g ` R ) )
314 313 ad5ant14 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ x C_ I ) /\ k e. I ) -> ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) finSupp ( 0g ` R ) )
315 10 100 299 301 306 314 gsumcl 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ x C_ I ) /\ k e. I ) -> ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) e. ( Base ` R ) )
316 215 315 sylanl2 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( x u. { z } ) C_ I ) /\ k e. I ) -> ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) e. ( Base ` R ) )
317 265 279 sylanl2 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( x u. { z } ) C_ I ) /\ k e. I ) -> ( ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` z ) ) ( .r ` R ) ( z M k ) ) e. ( Base ` R ) )
318 simpllr 
 |-  ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) -> M : ( I X. I ) --> ( Base ` R ) )
319 simpl 
 |-  ( ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) -> i e. I )
320 318 319 anim12i 
 |-  ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) -> ( M : ( I X. I ) --> ( Base ` R ) /\ i e. I ) )
321 320 adantr 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( x u. { z } ) C_ I ) -> ( M : ( I X. I ) --> ( Base ` R ) /\ i e. I ) )
322 fovcdm 
 |-  ( ( M : ( I X. I ) --> ( Base ` R ) /\ i e. I /\ k e. I ) -> ( i M k ) e. ( Base ` R ) )
323 322 3expa 
 |-  ( ( ( M : ( I X. I ) --> ( Base ` R ) /\ i e. I ) /\ k e. I ) -> ( i M k ) e. ( Base ` R ) )
324 321 323 sylan 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( x u. { z } ) C_ I ) /\ k e. I ) -> ( i M k ) e. ( Base ` R ) )
325 10 200 298 316 317 324 abl32 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( x u. { z } ) C_ I ) /\ k e. I ) -> ( ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` z ) ) ( .r ` R ) ( z M k ) ) ) ( +g ` R ) ( i M k ) ) = ( ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) ( +g ` R ) ( ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` z ) ) ( .r ` R ) ( z M k ) ) ) )
326 325 adantlrl 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) /\ k e. I ) -> ( ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` z ) ) ( .r ` R ) ( z M k ) ) ) ( +g ` R ) ( i M k ) ) = ( ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) ( +g ` R ) ( ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` z ) ) ( .r ` R ) ( z M k ) ) ) )
327 326 adantlr 
 |-  ( ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) /\ -. z e. x ) /\ k e. I ) -> ( ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` z ) ) ( .r ` R ) ( z M k ) ) ) ( +g ` R ) ( i M k ) ) = ( ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) ( +g ` R ) ( ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` z ) ) ( .r ` R ) ( z M k ) ) ) )
328 295 327 eqtrd 
 |-  ( ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) /\ -. z e. x ) /\ k e. I ) -> ( ( R gsum ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) = ( ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) ( +g ` R ) ( ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` z ) ) ( .r ` R ) ( z M k ) ) ) )
329 328 ifeq1d 
 |-  ( ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) /\ -. z e. x ) /\ k e. I ) -> if ( j = i , ( ( R gsum ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , if ( j = z , ( z M k ) , ( j M k ) ) ) = if ( j = i , ( ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) ( +g ` R ) ( ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` z ) ) ( .r ` R ) ( z M k ) ) ) , if ( j = z , ( z M k ) , ( j M k ) ) ) )
330 329 3adant2 
 |-  ( ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) /\ -. z e. x ) /\ j e. I /\ k e. I ) -> if ( j = i , ( ( R gsum ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , if ( j = z , ( z M k ) , ( j M k ) ) ) = if ( j = i , ( ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) ( +g ` R ) ( ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` z ) ) ( .r ` R ) ( z M k ) ) ) , if ( j = z , ( z M k ) , ( j M k ) ) ) )
331 330 mpoeq3dva 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) /\ -. z e. x ) -> ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , if ( j = z , ( z M k ) , ( j M k ) ) ) ) = ( j e. I , k e. I |-> if ( j = i , ( ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) ( +g ` R ) ( ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` z ) ) ( .r ` R ) ( z M k ) ) ) , if ( j = z , ( z M k ) , ( j M k ) ) ) ) )
332 331 fveq2d 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) /\ -. z e. x ) -> ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , if ( j = z , ( z M k ) , ( j M k ) ) ) ) ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) ( +g ` R ) ( ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` z ) ) ( .r ` R ) ( z M k ) ) ) , if ( j = z , ( z M k ) , ( j M k ) ) ) ) ) )
333 eqid 
 |-  ( I maDet R ) = ( I maDet R )
334 1 simprbi 
 |-  ( R e. Field -> R e. CRing )
335 334 ad5antr 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) -> R e. CRing )
336 simp-4r 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) -> I e. Fin )
337 193 ad6antr 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ x C_ I ) /\ k e. I ) -> R e. Grp )
338 320 adantr 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ x C_ I ) -> ( M : ( I X. I ) --> ( Base ` R ) /\ i e. I ) )
339 338 323 sylan 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ x C_ I ) /\ k e. I ) -> ( i M k ) e. ( Base ` R ) )
340 10 200 grpcl 
 |-  ( ( R e. Grp /\ ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) e. ( Base ` R ) /\ ( i M k ) e. ( Base ` R ) ) -> ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) e. ( Base ` R ) )
341 337 315 339 340 syl3anc 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ x C_ I ) /\ k e. I ) -> ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) e. ( Base ` R ) )
342 228 341 sylanl2 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) /\ k e. I ) -> ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) e. ( Base ` R ) )
343 248 266 anim12i 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) -> ( M : ( I X. I ) --> ( Base ` R ) /\ z e. I ) )
344 343 276 sylan 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) /\ k e. I ) -> ( z M k ) e. ( Base ` R ) )
345 simp-5r 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) -> M : ( I X. I ) --> ( Base ` R ) )
346 345 198 syl3an1 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) /\ j e. I /\ k e. I ) -> ( j M k ) e. ( Base ` R ) )
347 266 273 sylan2 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) -> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` z ) ) e. ( Base ` R ) )
348 simplrl 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) -> i e. I )
349 265 ad2antll 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) -> z e. I )
350 simprl 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) -> i =/= z )
351 333 10 200 47 335 336 342 344 346 347 348 349 350 mdetero 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) -> ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) ( +g ` R ) ( ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` z ) ) ( .r ` R ) ( z M k ) ) ) , if ( j = z , ( z M k ) , ( j M k ) ) ) ) ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , if ( j = z , ( z M k ) , ( j M k ) ) ) ) ) )
352 351 adantr 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) /\ -. z e. x ) -> ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) ( +g ` R ) ( ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` z ) ) ( .r ` R ) ( z M k ) ) ) , if ( j = z , ( z M k ) , ( j M k ) ) ) ) ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , if ( j = z , ( z M k ) , ( j M k ) ) ) ) ) )
353 332 352 eqtrd 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) /\ -. z e. x ) -> ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , if ( j = z , ( z M k ) , ( j M k ) ) ) ) ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , if ( j = z , ( z M k ) , ( j M k ) ) ) ) ) )
354 iftrue 
 |-  ( j = z -> if ( j = z , ( z M k ) , ( j M k ) ) = ( z M k ) )
355 oveq1 
 |-  ( j = z -> ( j M k ) = ( z M k ) )
356 354 355 eqtr4d 
 |-  ( j = z -> if ( j = z , ( z M k ) , ( j M k ) ) = ( j M k ) )
357 iffalse 
 |-  ( -. j = z -> if ( j = z , ( z M k ) , ( j M k ) ) = ( j M k ) )
358 356 357 pm2.61i 
 |-  if ( j = z , ( z M k ) , ( j M k ) ) = ( j M k )
359 ifeq2 
 |-  ( if ( j = z , ( z M k ) , ( j M k ) ) = ( j M k ) -> if ( j = i , ( ( R gsum ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , if ( j = z , ( z M k ) , ( j M k ) ) ) = if ( j = i , ( ( R gsum ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) )
360 358 359 mp1i 
 |-  ( ( j e. I /\ k e. I ) -> if ( j = i , ( ( R gsum ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , if ( j = z , ( z M k ) , ( j M k ) ) ) = if ( j = i , ( ( R gsum ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) )
361 360 mpoeq3ia 
 |-  ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , if ( j = z , ( z M k ) , ( j M k ) ) ) ) = ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) )
362 361 fveq2i 
 |-  ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , if ( j = z , ( z M k ) , ( j M k ) ) ) ) ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) )
363 ifeq2 
 |-  ( if ( j = z , ( z M k ) , ( j M k ) ) = ( j M k ) -> if ( j = i , ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , if ( j = z , ( z M k ) , ( j M k ) ) ) = if ( j = i , ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) )
364 358 363 mp1i 
 |-  ( ( j e. I /\ k e. I ) -> if ( j = i , ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , if ( j = z , ( z M k ) , ( j M k ) ) ) = if ( j = i , ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) )
365 364 mpoeq3ia 
 |-  ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , if ( j = z , ( z M k ) , ( j M k ) ) ) ) = ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) )
366 365 fveq2i 
 |-  ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , if ( j = z , ( z M k ) , ( j M k ) ) ) ) ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) )
367 353 362 366 3eqtr3g 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( i =/= z /\ ( x u. { z } ) C_ I ) ) /\ -. z e. x ) -> ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) )
368 223 367 sylanl2 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( -. i e. ( x u. { z } ) /\ ( x u. { z } ) C_ I ) ) /\ -. z e. x ) -> ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) )
369 368 eqeq2d 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( -. i e. ( x u. { z } ) /\ ( x u. { z } ) C_ I ) ) /\ -. z e. x ) -> ( ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) <-> ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) ) )
370 369 biimprd 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( -. i e. ( x u. { z } ) /\ ( x u. { z } ) C_ I ) ) /\ -. z e. x ) -> ( ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) -> ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) ) )
371 218 370 embantd 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( -. i e. ( x u. { z } ) /\ ( x u. { z } ) C_ I ) ) /\ -. z e. x ) -> ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( -. i e. x /\ x C_ I ) ) -> ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) ) -> ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) ) )
372 371 expcom 
 |-  ( -. z e. x -> ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( -. i e. ( x u. { z } ) /\ ( x u. { z } ) C_ I ) ) -> ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( -. i e. x /\ x C_ I ) ) -> ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) ) -> ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) ) ) )
373 372 com23 
 |-  ( -. z e. x -> ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( -. i e. x /\ x C_ I ) ) -> ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) ) -> ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( -. i e. ( x u. { z } ) /\ ( x u. { z } ) C_ I ) ) -> ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) ) ) )
374 373 adantl 
 |-  ( ( x e. Fin /\ -. z e. x ) -> ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( -. i e. x /\ x C_ I ) ) -> ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) ) -> ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( -. i e. ( x u. { z } ) /\ ( x u. { z } ) C_ I ) ) -> ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) ) ) )
375 149 162 175 188 210 374 findcard2s 
 |-  ( ( I \ { i } ) e. Fin -> ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( -. i e. ( I \ { i } ) /\ ( I \ { i } ) C_ I ) ) -> ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. ( I \ { i } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) ) )
376 132 375 mpcom 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( -. i e. ( I \ { i } ) /\ ( I \ { i } ) C_ I ) ) -> ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. ( I \ { i } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) )
377 129 130 376 mpanr12 
 |-  ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) -> ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. ( I \ { i } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) )
378 377 adantlr 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( k e. I |-> ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) -> ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. ( I \ { i } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) )
379 eqid 
 |-  I = I
380 fconstmpt 
 |-  ( I X. { ( 0g ` R ) } ) = ( k e. I |-> ( 0g ` R ) )
381 380 eqeq2i 
 |-  ( ( k e. I |-> ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) <-> ( k e. I |-> ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( k e. I |-> ( 0g ` R ) ) )
382 ovex 
 |-  ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) e. _V
383 382 rgenw 
 |-  A. k e. I ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) e. _V
384 mpteqb 
 |-  ( A. k e. I ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) e. _V -> ( ( k e. I |-> ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( k e. I |-> ( 0g ` R ) ) <-> A. k e. I ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) = ( 0g ` R ) ) )
385 383 384 ax-mp 
 |-  ( ( k e. I |-> ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( k e. I |-> ( 0g ` R ) ) <-> A. k e. I ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) = ( 0g ` R ) )
386 381 385 bitri 
 |-  ( ( k e. I |-> ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) <-> A. k e. I ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) = ( 0g ` R ) )
387 225 ad5antr 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ k e. I ) -> R e. CMnd )
388 simp-4r 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ k e. I ) -> I e. Fin )
389 eqid 
 |-  ( n e. I |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) = ( n e. I |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) )
390 307 389 fnmpti 
 |-  ( n e. I |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) Fn I
391 390 a1i 
 |-  ( I e. Fin -> ( n e. I |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) Fn I )
392 id 
 |-  ( I e. Fin -> I e. Fin )
393 fvexd 
 |-  ( I e. Fin -> ( 0g ` R ) e. _V )
394 391 392 393 fndmfifsupp 
 |-  ( I e. Fin -> ( n e. I |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) finSupp ( 0g ` R ) )
395 394 ad4antlr 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ k e. I ) -> ( n e. I |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) finSupp ( 0g ` R ) )
396 simplrl 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ k e. I ) -> i e. I )
397 320 323 sylan 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ k e. I ) -> ( i M k ) e. ( Base ` R ) )
398 fveq2 
 |-  ( n = i -> ( f ` n ) = ( f ` i ) )
399 oveq1 
 |-  ( n = i -> ( n M k ) = ( i M k ) )
400 398 399 oveq12d 
 |-  ( n = i -> ( ( f ` n ) ( .r ` R ) ( n M k ) ) = ( ( f ` i ) ( .r ` R ) ( i M k ) ) )
401 400 oveq2d 
 |-  ( n = i -> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) = ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` i ) ( .r ` R ) ( i M k ) ) ) )
402 simpll 
 |-  ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) -> R e. Field )
403 2 237 anim12i 
 |-  ( ( R e. Field /\ ( f : I --> ( Base ` R ) /\ i e. I ) ) -> ( R e. DivRing /\ ( f ` i ) e. ( Base ` R ) ) )
404 403 anassrs 
 |-  ( ( ( R e. Field /\ f : I --> ( Base ` R ) ) /\ i e. I ) -> ( R e. DivRing /\ ( f ` i ) e. ( Base ` R ) ) )
405 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
406 10 100 47 405 240 drnginvrl 
 |-  ( ( R e. DivRing /\ ( f ` i ) e. ( Base ` R ) /\ ( f ` i ) =/= ( 0g ` R ) ) -> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` i ) ) = ( 1r ` R ) )
407 406 3expa 
 |-  ( ( ( R e. DivRing /\ ( f ` i ) e. ( Base ` R ) ) /\ ( f ` i ) =/= ( 0g ` R ) ) -> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` i ) ) = ( 1r ` R ) )
408 404 407 sylan 
 |-  ( ( ( ( R e. Field /\ f : I --> ( Base ` R ) ) /\ i e. I ) /\ ( f ` i ) =/= ( 0g ` R ) ) -> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` i ) ) = ( 1r ` R ) )
409 408 anasss 
 |-  ( ( ( R e. Field /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) -> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` i ) ) = ( 1r ` R ) )
410 409 oveq1d 
 |-  ( ( ( R e. Field /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) -> ( ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` i ) ) ( .r ` R ) ( i M k ) ) = ( ( 1r ` R ) ( .r ` R ) ( i M k ) ) )
411 402 410 sylanl1 
 |-  ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) -> ( ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` i ) ) ( .r ` R ) ( i M k ) ) = ( ( 1r ` R ) ( .r ` R ) ( i M k ) ) )
412 411 adantr 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ k e. I ) -> ( ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` i ) ) ( .r ` R ) ( i M k ) ) = ( ( 1r ` R ) ( .r ` R ) ( i M k ) ) )
413 4 ad5antr 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ k e. I ) -> R e. Ring )
414 245 adantr 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ k e. I ) -> ( ( invr ` R ) ` ( f ` i ) ) e. ( Base ` R ) )
415 237 ad2ant2lr 
 |-  ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) -> ( f ` i ) e. ( Base ` R ) )
416 415 adantr 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ k e. I ) -> ( f ` i ) e. ( Base ` R ) )
417 10 47 ringass 
 |-  ( ( R e. Ring /\ ( ( ( invr ` R ) ` ( f ` i ) ) e. ( Base ` R ) /\ ( f ` i ) e. ( Base ` R ) /\ ( i M k ) e. ( Base ` R ) ) ) -> ( ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` i ) ) ( .r ` R ) ( i M k ) ) = ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` i ) ( .r ` R ) ( i M k ) ) ) )
418 413 414 416 397 417 syl13anc 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ k e. I ) -> ( ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` i ) ) ( .r ` R ) ( i M k ) ) = ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` i ) ( .r ` R ) ( i M k ) ) ) )
419 4 adantr 
 |-  ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) -> R e. Ring )
420 419 3ad2ant1 
 |-  ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ i e. I /\ k e. I ) -> R e. Ring )
421 322 3adant1l 
 |-  ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ i e. I /\ k e. I ) -> ( i M k ) e. ( Base ` R ) )
422 10 47 405 ringlidm 
 |-  ( ( R e. Ring /\ ( i M k ) e. ( Base ` R ) ) -> ( ( 1r ` R ) ( .r ` R ) ( i M k ) ) = ( i M k ) )
423 420 421 422 syl2anc 
 |-  ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ i e. I /\ k e. I ) -> ( ( 1r ` R ) ( .r ` R ) ( i M k ) ) = ( i M k ) )
424 423 ad5ant145 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ i e. I ) /\ k e. I ) -> ( ( 1r ` R ) ( .r ` R ) ( i M k ) ) = ( i M k ) )
425 424 adantlrr 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ k e. I ) -> ( ( 1r ` R ) ( .r ` R ) ( i M k ) ) = ( i M k ) )
426 412 418 425 3eqtr3d 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ k e. I ) -> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` i ) ( .r ` R ) ( i M k ) ) ) = ( i M k ) )
427 401 426 sylan9eqr 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ k e. I ) /\ n = i ) -> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) = ( i M k ) )
428 10 200 387 388 395 254 396 397 427 gsumdifsnd 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ k e. I ) -> ( R gsum ( n e. I |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( ( R gsum ( n e. ( I \ { i } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) )
429 ovex 
 |-  ( ( f ` n ) ( .r ` R ) ( n M k ) ) e. _V
430 eqid 
 |-  ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) = ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) )
431 429 430 fnmpti 
 |-  ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) Fn I
432 431 a1i 
 |-  ( I e. Fin -> ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) Fn I )
433 432 392 393 fndmfifsupp 
 |-  ( I e. Fin -> ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) finSupp ( 0g ` R ) )
434 433 ad4antlr 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ k e. I ) -> ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) finSupp ( 0g ` R ) )
435 10 100 47 413 388 414 252 434 gsummulc2 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ k e. I ) -> ( R gsum ( n e. I |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) )
436 428 435 eqtr3d 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ k e. I ) -> ( ( R gsum ( n e. ( I \ { i } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) = ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) )
437 436 adantr 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ k e. I ) /\ ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) = ( 0g ` R ) ) -> ( ( R gsum ( n e. ( I \ { i } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) = ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) )
438 oveq2 
 |-  ( ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) = ( 0g ` R ) -> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( 0g ` R ) ) )
439 438 adantl 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ k e. I ) /\ ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) = ( 0g ` R ) ) -> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( 0g ` R ) ) )
440 4 ad4antr 
 |-  ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) -> R e. Ring )
441 10 47 100 ringrz 
 |-  ( ( R e. Ring /\ ( ( invr ` R ) ` ( f ` i ) ) e. ( Base ` R ) ) -> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
442 440 245 441 syl2anc 
 |-  ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) -> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
443 442 ad2antrr 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ k e. I ) /\ ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) = ( 0g ` R ) ) -> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
444 437 439 443 3eqtrd 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ k e. I ) /\ ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) = ( 0g ` R ) ) -> ( ( R gsum ( n e. ( I \ { i } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) = ( 0g ` R ) )
445 444 ifeq1d 
 |-  ( ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ k e. I ) /\ ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) = ( 0g ` R ) ) -> if ( j = i , ( ( R gsum ( n e. ( I \ { i } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) = if ( j = i , ( 0g ` R ) , ( j M k ) ) )
446 445 ex 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ k e. I ) -> ( ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) = ( 0g ` R ) -> if ( j = i , ( ( R gsum ( n e. ( I \ { i } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) = if ( j = i , ( 0g ` R ) , ( j M k ) ) ) )
447 446 ralimdva 
 |-  ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) -> ( A. k e. I ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) = ( 0g ` R ) -> A. k e. I if ( j = i , ( ( R gsum ( n e. ( I \ { i } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) = if ( j = i , ( 0g ` R ) , ( j M k ) ) ) )
448 447 imp 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ A. k e. I ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) = ( 0g ` R ) ) -> A. k e. I if ( j = i , ( ( R gsum ( n e. ( I \ { i } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) = if ( j = i , ( 0g ` R ) , ( j M k ) ) )
449 386 448 sylan2b 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( k e. I |-> ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) ) -> A. k e. I if ( j = i , ( ( R gsum ( n e. ( I \ { i } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) = if ( j = i , ( 0g ` R ) , ( j M k ) ) )
450 449 379 jctil 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( k e. I |-> ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) ) -> ( I = I /\ A. k e. I if ( j = i , ( ( R gsum ( n e. ( I \ { i } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) = if ( j = i , ( 0g ` R ) , ( j M k ) ) ) )
451 450 ralrimivw 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( k e. I |-> ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) ) -> A. j e. I ( I = I /\ A. k e. I if ( j = i , ( ( R gsum ( n e. ( I \ { i } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) = if ( j = i , ( 0g ` R ) , ( j M k ) ) ) )
452 mpoeq123 
 |-  ( ( I = I /\ A. j e. I ( I = I /\ A. k e. I if ( j = i , ( ( R gsum ( n e. ( I \ { i } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) = if ( j = i , ( 0g ` R ) , ( j M k ) ) ) ) -> ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. ( I \ { i } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) = ( j e. I , k e. I |-> if ( j = i , ( 0g ` R ) , ( j M k ) ) ) )
453 379 451 452 sylancr 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ ( k e. I |-> ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) ) -> ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. ( I \ { i } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) = ( j e. I , k e. I |-> if ( j = i , ( 0g ` R ) , ( j M k ) ) ) )
454 453 an32s 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( k e. I |-> ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) -> ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. ( I \ { i } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) = ( j e. I , k e. I |-> if ( j = i , ( 0g ` R ) , ( j M k ) ) ) )
455 454 fveq2d 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( k e. I |-> ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) -> ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsum ( n e. ( I \ { i } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( 0g ` R ) , ( j M k ) ) ) ) )
456 334 ad3antrrr 
 |-  ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) -> R e. CRing )
457 simplr 
 |-  ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) -> I e. Fin )
458 simpllr 
 |-  ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) -> M : ( I X. I ) --> ( Base ` R ) )
459 458 198 syl3an1 
 |-  ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) /\ j e. I /\ k e. I ) -> ( j M k ) e. ( Base ` R ) )
460 simprl 
 |-  ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) -> i e. I )
461 333 10 100 456 457 459 460 mdetr0 
 |-  ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) -> ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( 0g ` R ) , ( j M k ) ) ) ) = ( 0g ` R ) )
462 461 ad4ant14 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( k e. I |-> ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) -> ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( 0g ` R ) , ( j M k ) ) ) ) = ( 0g ` R ) )
463 378 455 462 3eqtrd 
 |-  ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( k e. I |-> ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) -> ( ( I maDet R ) ` M ) = ( 0g ` R ) )
464 463 rexlimdvaa 
 |-  ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( k e. I |-> ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) ) -> ( E. i e. I ( f ` i ) =/= ( 0g ` R ) -> ( ( I maDet R ) ` M ) = ( 0g ` R ) ) )
465 464 expimpd 
 |-  ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) -> ( ( ( k e. I |-> ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) /\ E. i e. I ( f ` i ) =/= ( 0g ` R ) ) -> ( ( I maDet R ) ` M ) = ( 0g ` R ) ) )
466 128 465 sylan2d 
 |-  ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) -> ( ( ( k e. I |-> ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) /\ -. f = ( I X. { ( 0g ` R ) } ) ) -> ( ( I maDet R ) ` M ) = ( 0g ` R ) ) )
467 32 466 sylan2 
 |-  ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f e. ( ( Base ` R ) ^m I ) ) -> ( ( ( k e. I |-> ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) /\ -. f = ( I X. { ( 0g ` R ) } ) ) -> ( ( I maDet R ) ` M ) = ( 0g ` R ) ) )
468 467 rexlimdva 
 |-  ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) -> ( E. f e. ( ( Base ` R ) ^m I ) ( ( k e. I |-> ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) /\ -. f = ( I X. { ( 0g ` R ) } ) ) -> ( ( I maDet R ) ` M ) = ( 0g ` R ) ) )
469 9 468 sylan2 
 |-  ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) -> ( E. f e. ( ( Base ` R ) ^m I ) ( ( k e. I |-> ( R gsum ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) /\ -. f = ( I X. { ( 0g ` R ) } ) ) -> ( ( I maDet R ) ` M ) = ( 0g ` R ) ) )
470 115 469 sylbid 
 |-  ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) -> ( -. curry M LIndF ( R freeLMod I ) -> ( ( I maDet R ) ` M ) = ( 0g ` R ) ) )