Theorem matunitlindflem1 33405

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

Assertion

Ref	Expression
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 of Theorem matunitlindflem1

Dummy variables x f y z i j k n are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		isfld 18756	. . . . 5 |- ( R e. Field <-> ( R e. DivRing /\ R e. CRing ) )
2	1	simplbi 476	. . . 4 |- ( R e. Field -> R e. DivRing )
3		drngring 18754	. . . 4 |- ( R e. DivRing -> R e. Ring )
4	2, 3	syl 17	. . 3 |- ( R e. Field -> R e. Ring )
5		eqid 2622	. . . . . . . . 9 |- ( R freeLMod I ) = ( R freeLMod I )
6	5	frlmlmod 20093	. . . . . . . 8 |- ( ( R e. Ring /\ I e. ( Fin \ { (/) } ) ) -> ( R freeLMod I ) e. LMod )
7	6	adantlr 751	. . . . . . 7 |- ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) -> ( R freeLMod I ) e. LMod )
8		simpr 477	. . . . . . 7 |- ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) -> I e. ( Fin \ { (/) } ) )
9		eldifi 3732	. . . . . . . . . 10 |- ( I e. ( Fin \ { (/) } ) -> I e. Fin )
10		eqid 2622	. . . . . . . . . . 11 |- ( Base ` R ) = ( Base ` R )
11	5, 10	frlmfibas 20105	. . . . . . . . . 10 |- ( ( R e. Ring /\ I e. Fin ) -> ( ( Base ` R ) ^m I ) = ( Base ` ( R freeLMod I ) ) )
12	9, 11	sylan2 491	. . . . . . . . 9 |- ( ( R e. Ring /\ I e. ( Fin \ { (/) } ) ) -> ( ( Base ` R ) ^m I ) = ( Base ` ( R freeLMod I ) ) )
13		fvex 6201	. . . . . . . . . 10 |- ( Base ` R ) e. _V
14		curf 33387	. . . . . . . . . 10 |- ( ( M : ( I X. I ) --> ( Base ` R ) /\ I e. ( Fin \ { (/) } ) /\ ( Base ` R ) e. _V ) -> curry M : I --> ( ( Base ` R ) ^m I ) )
15	13, 14	mp3an3 1413	. . . . . . . . 9 |- ( ( M : ( I X. I ) --> ( Base ` R ) /\ I e. ( Fin \ { (/) } ) ) -> curry M : I --> ( ( Base ` R ) ^m I ) )
16		feq3 6028	. . . . . . . . . 10 |- ( ( ( 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 501	. . . . . . . . 9 |- ( ( ( ( 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 494	. . . . . . . 8 |- ( ( ( 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 874	. . . . . . 7 |- ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) -> curry M : I --> ( Base ` ( R freeLMod I ) ) )
20		eqid 2622	. . . . . . . 8 |- ( Base ` ( R freeLMod I ) ) = ( Base ` ( R freeLMod I ) )
21		eqid 2622	. . . . . . . 8 |- (Scalar ` ( R freeLMod I ) ) = (Scalar ` ( R freeLMod I ) )
22		eqid 2622	. . . . . . . 8 |- ( .s ` ( R freeLMod I ) ) = ( .s ` ( R freeLMod I ) )
23		eqid 2622	. . . . . . . 8 |- ( 0g ` ( R freeLMod I ) ) = ( 0g ` ( R freeLMod I ) )
24		eqid 2622	. . . . . . . 8 |- ( 0g ` (Scalar ` ( R freeLMod I ) ) ) = ( 0g ` (Scalar ` ( R freeLMod I ) ) )
25		eqid 2622	. . . . . . . 8 |- ( Base ` ( (Scalar ` ( R freeLMod I ) ) freeLMod I ) ) = ( Base ` ( (Scalar ` ( R freeLMod I ) ) freeLMod I ) )
26	20, 21, 22, 23, 24, 25	islindf4 20177	. . . . . . 7 |- ( ( ( 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 ) gsumg ( 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 1326	. . . . . 6 |- ( ( ( 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 ) gsumg ( f oF ( .s ` ( R freeLMod I ) )curry M ) ) = ( 0g ` ( R freeLMod I ) ) -> f = ( I X. { ( 0g ` (Scalar ` ( R freeLMod I ) ) ) } ) ) ) )
28	5	frlmsca 20097	. . . . . . . . . . 11 |- ( ( R e. Ring /\ I e. ( Fin \ { (/) } ) ) -> R = (Scalar ` ( R freeLMod I ) ) )
29	28	oveq1d 6665	. . . . . . . . . 10 |- ( ( R e. Ring /\ I e. ( Fin \ { (/) } ) ) -> ( R freeLMod I ) = ( (Scalar ` ( R freeLMod I ) ) freeLMod I ) )
30	29	fveq2d 6195	. . . . . . . . 9 |- ( ( R e. Ring /\ I e. ( Fin \ { (/) } ) ) -> ( Base ` ( R freeLMod I ) ) = ( Base ` ( (Scalar ` ( R freeLMod I ) ) freeLMod I ) ) )
31	12, 30	eqtrd 2656	. . . . . . . 8 |- ( ( R e. Ring /\ I e. ( Fin \ { (/) } ) ) -> ( ( Base ` R ) ^m I ) = ( Base ` ( (Scalar ` ( R freeLMod I ) ) freeLMod I ) ) )
32	31	adantlr 751	. . . . . . 7 |- ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) -> ( ( Base ` R ) ^m I ) = ( Base ` ( (Scalar ` ( R freeLMod I ) ) freeLMod I ) ) )
33		elmapi 7879	. . . . . . . . . 10 |- ( f e. ( ( Base ` R ) ^m I ) -> f : I --> ( Base ` R ) )
34		ffn 6045	. . . . . . . . . . . . . . 15 |- ( f : I --> ( Base ` R ) -> f Fn I )
35	34	adantl 482	. . . . . . . . . . . . . 14 |- ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) -> f Fn I )
36	19	ffnd 6046	. . . . . . . . . . . . . . 15 |- ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) -> curry M Fn I )
37	36	adantr 481	. . . . . . . . . . . . . 14 |- ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) -> curry M Fn I )
38		simplr 792	. . . . . . . . . . . . . 14 |- ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) -> I e. ( Fin \ { (/) } ) )
39		inidm 3822	. . . . . . . . . . . . . 14 |- ( I i^i I ) = I
40		eqidd 2623	. . . . . . . . . . . . . 14 |- ( ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) /\ n e. I ) -> ( f ` n ) = ( f ` n ) )
41		eqidd 2623	. . . . . . . . . . . . . 14 |- ( ( ( ( ( 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 ) )
42	35, 37, 38, 38, 39, 40, 41	offval 6904	. . . . . . . . . . . . 13 |- ( ( ( ( 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 ) ) ) )
43		simpllr 799	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) /\ n e. I ) -> I e. ( Fin \ { (/) } ) )
44		ffvelrn 6357	. . . . . . . . . . . . . . . . 17 |- ( ( f : I --> ( Base ` R ) /\ n e. I ) -> ( f ` n ) e. ( Base ` R ) )
45	44	adantll 750	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) /\ n e. I ) -> ( f ` n ) e. ( Base ` R ) )
46	19	ffvelrnda 6359	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ n e. I ) -> (curry M ` n ) e. ( Base ` ( R freeLMod I ) ) )
47	46	adantlr 751	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( 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 ) ) )
48		eqid 2622	. . . . . . . . . . . . . . . 16 |- ( .r ` R ) = ( .r ` R )
49	5, 20, 10, 43, 45, 47, 22, 48	frlmvscafval 20109	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( 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 ) ) )
50		fvex 6201	. . . . . . . . . . . . . . . . 17 |- ( f ` n ) e. _V
51		fnconstg 6093	. . . . . . . . . . . . . . . . 17 |- ( ( f ` n ) e. _V -> ( I X. { ( f ` n ) } ) Fn I )
52	50, 51	mp1i 13	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( 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 )
53	15	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( M : ( I X. I ) --> ( Base ` R ) /\ I e. ( Fin \ { (/) } ) ) /\ n e. I ) -> (curry M ` n ) e. ( ( Base ` R ) ^m I ) )
54		elmapfn 7880	. . . . . . . . . . . . . . . . . . 19 |- ( (curry M ` n ) e. ( ( Base ` R ) ^m I ) -> (curry M ` n ) Fn I )
55	53, 54	syl 17	. . . . . . . . . . . . . . . . . 18 |- ( ( ( M : ( I X. I ) --> ( Base ` R ) /\ I e. ( Fin \ { (/) } ) ) /\ n e. I ) -> (curry M ` n ) Fn I )
56	55	adantlll 754	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ n e. I ) -> (curry M ` n ) Fn I )
57	56	adantlr 751	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) /\ n e. I ) -> (curry M ` n ) Fn I )
58	50	fvconst2 6469	. . . . . . . . . . . . . . . . 17 |- ( k e. I -> ( ( I X. { ( f ` n ) } ) ` k ) = ( f ` n ) )
59	58	adantl 482	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( 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 ) )
60		ffn 6045	. . . . . . . . . . . . . . . . . . . 20 |- ( M : ( I X. I ) --> ( Base ` R ) -> M Fn ( I X. I ) )
61	60	anim2i 593	. . . . . . . . . . . . . . . . . . 19 |- ( ( I e. ( Fin \ { (/) } ) /\ M : ( I X. I ) --> ( Base ` R ) ) -> ( I e. ( Fin \ { (/) } ) /\ M Fn ( I X. I ) ) )
62	61	ancoms 469	. . . . . . . . . . . . . . . . . 18 |- ( ( M : ( I X. I ) --> ( Base ` R ) /\ I e. ( Fin \ { (/) } ) ) -> ( I e. ( Fin \ { (/) } ) /\ M Fn ( I X. I ) ) )
63	62	ad4ant23 1297	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) -> ( I e. ( Fin \ { (/) } ) /\ M Fn ( I X. I ) ) )
64		curfv 33389	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( M Fn ( I X. I ) /\ n e. I /\ k e. I ) /\ I e. ( Fin \ { (/) } ) ) -> ( (curry M ` n ) ` k ) = ( n M k ) )
65	64	3exp1 1283	. . . . . . . . . . . . . . . . . . 19 |- ( M Fn ( I X. I ) -> ( n e. I -> ( k e. I -> ( I e. ( Fin \ { (/) } ) -> ( (curry M ` n ) ` k ) = ( n M k ) ) ) ) )
66	65	com4r 94	. . . . . . . . . . . . . . . . . 18 |- ( I e. ( Fin \ { (/) } ) -> ( M Fn ( I X. I ) -> ( n e. I -> ( k e. I -> ( (curry M ` n ) ` k ) = ( n M k ) ) ) ) )
67	66	imp41 619	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( I e. ( Fin \ { (/) } ) /\ M Fn ( I X. I ) ) /\ n e. I ) /\ k e. I ) -> ( (curry M ` n ) ` k ) = ( n M k ) )
68	63, 67	sylanl1 682	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( 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 ) )
69	52, 57, 43, 43, 39, 59, 68	offval 6904	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( 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 ) ) ) )
70	49, 69	eqtrd 2656	. . . . . . . . . . . . . 14 |- ( ( ( ( ( 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 ) ) ) )
71	70	mpteq2dva 4744	. . . . . . . . . . . . 13 |- ( ( ( ( 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 ) ) ) ) )
72	42, 71	eqtrd 2656	. . . . . . . . . . . 12 |- ( ( ( ( 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 ) ) ) ) )
73	72	oveq2d 6666	. . . . . . . . . . 11 |- ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) -> ( ( R freeLMod I ) gsumg ( f oF ( .s ` ( R freeLMod I ) )curry M ) ) = ( ( R freeLMod I ) gsumg ( n e. I |-> ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) )
74		simplll 798	. . . . . . . . . . . 12 |- ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) -> R e. Ring )
75		simp-4l 806	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ f : I --> ( Base ` R ) ) /\ n e. I ) /\ k e. I ) -> R e. Ring )
76	44	ad4ant23 1297	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ f : I --> ( Base ` R ) ) /\ n e. I ) /\ k e. I ) -> ( f ` n ) e. ( Base ` R ) )
77		fovrn 6804	. . . . . . . . . . . . . . . . 17 |- ( ( M : ( I X. I ) --> ( Base ` R ) /\ n e. I /\ k e. I ) -> ( n M k ) e. ( Base ` R ) )
78	77	ad5ant245 1307	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( 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 ) )
79	10, 48	ringcl 18561	. . . . . . . . . . . . . . . 16 |- ( ( R e. Ring /\ ( f ` n ) e. ( Base ` R ) /\ ( n M k ) e. ( Base ` R ) ) -> ( ( f ` n ) ( .r ` R ) ( n M k ) ) e. ( Base ` R ) )
80	75, 76, 78, 79	syl3anc 1326	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( 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 ) )
81		eqid 2622	. . . . . . . . . . . . . . 15 |- ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) = ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) )
82	80, 81	fmptd 6385	. . . . . . . . . . . . . 14 |- ( ( ( ( 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 ) )
83	82	adantllr 755	. . . . . . . . . . . . 13 |- ( ( ( ( ( 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 ) )
84		elmapg 7870	. . . . . . . . . . . . . . . . 17 |- ( ( ( 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 ) ) )
85	13, 84	mpan 706	. . . . . . . . . . . . . . . 16 |- ( 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 ) ) )
86	85	adantl 482	. . . . . . . . . . . . . . 15 |- ( ( 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 ) ) )
87	12	eleq2d 2687	. . . . . . . . . . . . . . 15 |- ( ( 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 ) ) ) )
88	86, 87	bitr3d 270	. . . . . . . . . . . . . 14 |- ( ( 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 ) ) ) )
89	88	ad5ant13 1301	. . . . . . . . . . . . 13 |- ( ( ( ( ( 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 ) ) ) )
90	83, 89	mpbid 222	. . . . . . . . . . . 12 |- ( ( ( ( ( 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 ) ) )
91		mptexg 6484	. . . . . . . . . . . . . . . 16 |- ( I e. ( Fin \ { (/) } ) -> ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) e. _V )
92	91	ralrimivw 2967	. . . . . . . . . . . . . . 15 |- ( I e. ( Fin \ { (/) } ) -> A. n e. I ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) e. _V )
93		eqid 2622	. . . . . . . . . . . . . . . 16 |- ( 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 ) ) ) )
94	93	fnmpt 6020	. . . . . . . . . . . . . . 15 |- ( 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 )
95	92, 94	syl 17	. . . . . . . . . . . . . 14 |- ( I e. ( Fin \ { (/) } ) -> ( n e. I |-> ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) Fn I )
96		fvexd 6203	. . . . . . . . . . . . . 14 |- ( I e. ( Fin \ { (/) } ) -> ( 0g ` ( R freeLMod I ) ) e. _V )
97	95, 9, 96	fndmfifsupp 8288	. . . . . . . . . . . . 13 |- ( I e. ( Fin \ { (/) } ) -> ( n e. I |-> ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) finSupp ( 0g ` ( R freeLMod I ) ) )
98	97	ad2antlr 763	. . . . . . . . . . . 12 |- ( ( ( ( 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 ) ) )
99	5, 20, 23, 38, 38, 74, 90, 98	frlmgsum 20111	. . . . . . . . . . 11 |- ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) -> ( ( R freeLMod I ) gsumg ( n e. I |-> ( k e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( k e. I |-> ( R gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) )
100	73, 99	eqtr2d 2657	. . . . . . . . . 10 |- ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f : I --> ( Base ` R ) ) -> ( k e. I |-> ( R gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( ( R freeLMod I ) gsumg ( f oF ( .s ` ( R freeLMod I ) )curry M ) ) )
101	33, 100	sylan2 491	. . . . . . . . 9 |- ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f e. ( ( Base ` R ) ^m I ) ) -> ( k e. I |-> ( R gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( ( R freeLMod I ) gsumg ( f oF ( .s ` ( R freeLMod I ) )curry M ) ) )
102		eqid 2622	. . . . . . . . . . 11 |- ( 0g ` R ) = ( 0g ` R )
103	5, 102	frlm0 20098	. . . . . . . . . 10 |- ( ( R e. Ring /\ I e. ( Fin \ { (/) } ) ) -> ( I X. { ( 0g ` R ) } ) = ( 0g ` ( R freeLMod I ) ) )
104	103	ad4ant13 1292	. . . . . . . . 9 |- ( ( ( ( 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 ) ) )
105	101, 104	eqeq12d 2637	. . . . . . . 8 |- ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f e. ( ( Base ` R ) ^m I ) ) -> ( ( k e. I |-> ( R gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) <-> ( ( R freeLMod I ) gsumg ( f oF ( .s ` ( R freeLMod I ) )curry M ) ) = ( 0g ` ( R freeLMod I ) ) ) )
106	28	fveq2d 6195	. . . . . . . . . . . 12 |- ( ( R e. Ring /\ I e. ( Fin \ { (/) } ) ) -> ( 0g ` R ) = ( 0g ` (Scalar ` ( R freeLMod I ) ) ) )
107	106	sneqd 4189	. . . . . . . . . . 11 |- ( ( R e. Ring /\ I e. ( Fin \ { (/) } ) ) -> { ( 0g ` R ) } = { ( 0g ` (Scalar ` ( R freeLMod I ) ) ) } )
108	107	xpeq2d 5139	. . . . . . . . . 10 |- ( ( R e. Ring /\ I e. ( Fin \ { (/) } ) ) -> ( I X. { ( 0g ` R ) } ) = ( I X. { ( 0g ` (Scalar ` ( R freeLMod I ) ) ) } ) )
109	108	eqeq2d 2632	. . . . . . . . 9 |- ( ( R e. Ring /\ I e. ( Fin \ { (/) } ) ) -> ( f = ( I X. { ( 0g ` R ) } ) <-> f = ( I X. { ( 0g ` (Scalar ` ( R freeLMod I ) ) ) } ) ) )
110	109	ad4ant13 1292	. . . . . . . 8 |- ( ( ( ( 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 ) ) ) } ) ) )
111	105, 110	imbi12d 334	. . . . . . 7 |- ( ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) /\ f e. ( ( Base ` R ) ^m I ) ) -> ( ( ( k e. I |-> ( R gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) -> f = ( I X. { ( 0g ` R ) } ) ) <-> ( ( ( R freeLMod I ) gsumg ( f oF ( .s ` ( R freeLMod I ) )curry M ) ) = ( 0g ` ( R freeLMod I ) ) -> f = ( I X. { ( 0g ` (Scalar ` ( R freeLMod I ) ) ) } ) ) ) )
112	32, 111	raleqbidva 3154	. . . . . 6 |- ( ( ( R e. Ring /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) -> ( A. f e. ( ( Base ` R ) ^m I ) ( ( k e. I |-> ( R gsumg ( 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 ) gsumg ( f oF ( .s ` ( R freeLMod I ) )curry M ) ) = ( 0g ` ( R freeLMod I ) ) -> f = ( I X. { ( 0g ` (Scalar ` ( R freeLMod I ) ) ) } ) ) ) )
113	27, 112	bitr4d 271	. . . . 5 |- ( ( ( 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 gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) -> f = ( I X. { ( 0g ` R ) } ) ) ) )
114	113	notbid 308	. . . 4 |- ( ( ( 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 gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) -> f = ( I X. { ( 0g ` R ) } ) ) ) )
115		rexanali 2998	. . . 4 |- ( E. f e. ( ( Base ` R ) ^m I ) ( ( k e. I |-> ( R gsumg ( 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 gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) -> f = ( I X. { ( 0g ` R ) } ) ) )
116	114, 115	syl6bbr 278	. . 3 |- ( ( ( 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 gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) /\ -. f = ( I X. { ( 0g ` R ) } ) ) ) )
117	4, 116	sylanl1 682	. 2 |- ( ( ( 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 gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) /\ -. f = ( I X. { ( 0g ` R ) } ) ) ) )
118		fconstfv 6476	. . . . . . . . . . . 12 |- ( f : I --> { ( 0g ` R ) } <-> ( f Fn I /\ A. i e. I ( f ` i ) = ( 0g ` R ) ) )
119		fvex 6201	. . . . . . . . . . . . 13 |- ( 0g ` R ) e. _V
120	119	fconst2 6470	. . . . . . . . . . . 12 |- ( f : I --> { ( 0g ` R ) } <-> f = ( I X. { ( 0g ` R ) } ) )
121	118, 120	sylbb1 227	. . . . . . . . . . 11 |- ( ( f Fn I /\ A. i e. I ( f ` i ) = ( 0g ` R ) ) -> f = ( I X. { ( 0g ` R ) } ) )
122	121	ex 450	. . . . . . . . . 10 |- ( f Fn I -> ( A. i e. I ( f ` i ) = ( 0g ` R ) -> f = ( I X. { ( 0g ` R ) } ) ) )
123	122	con3d 148	. . . . . . . . 9 |- ( f Fn I -> ( -. f = ( I X. { ( 0g ` R ) } ) -> -. A. i e. I ( f ` i ) = ( 0g ` R ) ) )
124		df-ne 2795	. . . . . . . . . . 11 |- ( ( f ` i ) =/= ( 0g ` R ) <-> -. ( f ` i ) = ( 0g ` R ) )
125	124	rexbii 3041	. . . . . . . . . 10 |- ( E. i e. I ( f ` i ) =/= ( 0g ` R ) <-> E. i e. I -. ( f ` i ) = ( 0g ` R ) )
126		rexnal 2995	. . . . . . . . . 10 |- ( E. i e. I -. ( f ` i ) = ( 0g ` R ) <-> -. A. i e. I ( f ` i ) = ( 0g ` R ) )
127	125, 126	bitri 264	. . . . . . . . 9 |- ( E. i e. I ( f ` i ) =/= ( 0g ` R ) <-> -. A. i e. I ( f ` i ) = ( 0g ` R ) )
128	123, 127	syl6ibr 242	. . . . . . . 8 |- ( f Fn I -> ( -. f = ( I X. { ( 0g ` R ) } ) -> E. i e. I ( f ` i ) =/= ( 0g ` R ) ) )
129	34, 128	syl 17	. . . . . . 7 |- ( f : I --> ( Base ` R ) -> ( -. f = ( I X. { ( 0g ` R ) } ) -> E. i e. I ( f ` i ) =/= ( 0g ` R ) ) )
130	129	adantl 482	. . . . . 6 |- ( ( ( ( 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 ) ) )
131		neldifsn 4321	. . . . . . . . . . 11 |- -. i e. ( I \ { i } )
132		difss 3737	. . . . . . . . . . 11 |- ( I \ { i } ) C_ I
133		diffi 8192	. . . . . . . . . . . . 13 |- ( I e. Fin -> ( I \ { i } ) e. Fin )
134	133	ad4antlr 769	. . . . . . . . . . . 12 |- ( ( ( ( ( ( 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 )
135		eleq2 2690	. . . . . . . . . . . . . . . . 17 |- ( y = (/) -> ( i e. y <-> i e. (/) ) )
136	135	notbid 308	. . . . . . . . . . . . . . . 16 |- ( y = (/) -> ( -. i e. y <-> -. i e. (/) ) )
137		sseq1 3626	. . . . . . . . . . . . . . . 16 |- ( y = (/) -> ( y C_ I <-> (/) C_ I ) )
138	136, 137	anbi12d 747	. . . . . . . . . . . . . . 15 |- ( y = (/) -> ( ( -. i e. y /\ y C_ I ) <-> ( -. i e. (/) /\ (/) C_ I ) ) )
139	138	anbi2d 740	. . . . . . . . . . . . . 14 |- ( 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 ) ) ) )
140		mpteq1 4737	. . . . . . . . . . . . . . . . . . . . . 22 |- ( 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 ) ) ) ) )
141		mpt0 6021	. . . . . . . . . . . . . . . . . . . . . 22 |- ( n e. (/) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) = (/)
142	140, 141	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . 21 |- ( y = (/) -> ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) = (/) )
143	142	oveq2d 6666	. . . . . . . . . . . . . . . . . . . 20 |- ( y = (/) -> ( R gsumg ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( R gsumg (/) ) )
144	102	gsum0 17278	. . . . . . . . . . . . . . . . . . . 20 |- ( R gsumg (/) ) = ( 0g ` R )
145	143, 144	syl6eq 2672	. . . . . . . . . . . . . . . . . . 19 |- ( y = (/) -> ( R gsumg ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( 0g ` R ) )
146	145	oveq1d 6665	. . . . . . . . . . . . . . . . . 18 |- ( y = (/) -> ( ( R gsumg ( 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 ) ) )
147	146	ifeq1d 4104	. . . . . . . . . . . . . . . . 17 |- ( y = (/) -> if ( j = i , ( ( R gsumg ( 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 ) ) )
148	147	mpt2eq3dv 6721	. . . . . . . . . . . . . . . 16 |- ( y = (/) -> ( j e. I , k e. I |-> if ( j = i , ( ( R gsumg ( 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 ) ) ) )
149	148	fveq2d 6195	. . . . . . . . . . . . . . 15 |- ( y = (/) -> ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsumg ( 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 ) ) ) ) )
150	149	eqeq2d 2632	. . . . . . . . . . . . . 14 |- ( y = (/) -> ( ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsumg ( 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 ) ) ) ) ) )
151	139, 150	imbi12d 334	. . . . . . . . . . . . 13 |- ( 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 gsumg ( 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 ) ) ) ) ) ) )
152		elequ2 2004	. . . . . . . . . . . . . . . . 17 |- ( y = x -> ( i e. y <-> i e. x ) )
153	152	notbid 308	. . . . . . . . . . . . . . . 16 |- ( y = x -> ( -. i e. y <-> -. i e. x ) )
154		sseq1 3626	. . . . . . . . . . . . . . . 16 |- ( y = x -> ( y C_ I <-> x C_ I ) )
155	153, 154	anbi12d 747	. . . . . . . . . . . . . . 15 |- ( y = x -> ( ( -. i e. y /\ y C_ I ) <-> ( -. i e. x /\ x C_ I ) ) )
156	155	anbi2d 740	. . . . . . . . . . . . . 14 |- ( 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 ) ) ) )
157		mpteq1 4737	. . . . . . . . . . . . . . . . . . . 20 |- ( 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 ) ) ) ) )
158	157	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19 |- ( y = x -> ( R gsumg ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( R gsumg ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) )
159	158	oveq1d 6665	. . . . . . . . . . . . . . . . . 18 |- ( y = x -> ( ( R gsumg ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) = ( ( R gsumg ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) )
160	159	ifeq1d 4104	. . . . . . . . . . . . . . . . 17 |- ( y = x -> if ( j = i , ( ( R gsumg ( 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 gsumg ( 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	mpt2eq3dv 6721	. . . . . . . . . . . . . . . 16 |- ( y = x -> ( j e. I , k e. I |-> if ( j = i , ( ( R gsumg ( 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 gsumg ( 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	161	fveq2d 6195	. . . . . . . . . . . . . . 15 |- ( y = x -> ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsumg ( 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 gsumg ( 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	162	eqeq2d 2632	. . . . . . . . . . . . . 14 |- ( y = x -> ( ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsumg ( 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 gsumg ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) ) )
164	156, 163	imbi12d 334	. . . . . . . . . . . . 13 |- ( 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 gsumg ( 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 gsumg ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) ) ) )
165		eleq2 2690	. . . . . . . . . . . . . . . . 17 |- ( y = ( x u. { z } ) -> ( i e. y <-> i e. ( x u. { z } ) ) )
166	165	notbid 308	. . . . . . . . . . . . . . . 16 |- ( y = ( x u. { z } ) -> ( -. i e. y <-> -. i e. ( x u. { z } ) ) )
167		sseq1 3626	. . . . . . . . . . . . . . . 16 |- ( y = ( x u. { z } ) -> ( y C_ I <-> ( x u. { z } ) C_ I ) )
168	166, 167	anbi12d 747	. . . . . . . . . . . . . . 15 |- ( y = ( x u. { z } ) -> ( ( -. i e. y /\ y C_ I ) <-> ( -. i e. ( x u. { z } ) /\ ( x u. { z } ) C_ I ) ) )
169	168	anbi2d 740	. . . . . . . . . . . . . 14 |- ( 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 ) ) ) )
170		mpteq1 4737	. . . . . . . . . . . . . . . . . . . 20 |- ( 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 ) ) ) ) )
171	170	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19 |- ( y = ( x u. { z } ) -> ( R gsumg ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( R gsumg ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) )
172	171	oveq1d 6665	. . . . . . . . . . . . . . . . . 18 |- ( y = ( x u. { z } ) -> ( ( R gsumg ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) = ( ( R gsumg ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) )
173	172	ifeq1d 4104	. . . . . . . . . . . . . . . . 17 |- ( y = ( x u. { z } ) -> if ( j = i , ( ( R gsumg ( 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 gsumg ( 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	mpt2eq3dv 6721	. . . . . . . . . . . . . . . 16 |- ( y = ( x u. { z } ) -> ( j e. I , k e. I |-> if ( j = i , ( ( R gsumg ( 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 gsumg ( 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	174	fveq2d 6195	. . . . . . . . . . . . . . 15 |- ( y = ( x u. { z } ) -> ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsumg ( 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 gsumg ( 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	175	eqeq2d 2632	. . . . . . . . . . . . . 14 |- ( y = ( x u. { z } ) -> ( ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsumg ( 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 gsumg ( 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 ) ) ) ) ) )
177	169, 176	imbi12d 334	. . . . . . . . . . . . 13 |- ( 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 gsumg ( 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 gsumg ( 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 ) ) ) ) ) ) )
178		eleq2 2690	. . . . . . . . . . . . . . . . 17 |- ( y = ( I \ { i } ) -> ( i e. y <-> i e. ( I \ { i } ) ) )
179	178	notbid 308	. . . . . . . . . . . . . . . 16 |- ( y = ( I \ { i } ) -> ( -. i e. y <-> -. i e. ( I \ { i } ) ) )
180		sseq1 3626	. . . . . . . . . . . . . . . 16 |- ( y = ( I \ { i } ) -> ( y C_ I <-> ( I \ { i } ) C_ I ) )
181	179, 180	anbi12d 747	. . . . . . . . . . . . . . 15 |- ( y = ( I \ { i } ) -> ( ( -. i e. y /\ y C_ I ) <-> ( -. i e. ( I \ { i } ) /\ ( I \ { i } ) C_ I ) ) )
182	181	anbi2d 740	. . . . . . . . . . . . . 14 |- ( 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 ) ) ) )
183		mpteq1 4737	. . . . . . . . . . . . . . . . . . . 20 |- ( 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 ) ) ) ) )
184	183	oveq2d 6666	. . . . . . . . . . . . . . . . . . 19 |- ( y = ( I \ { i } ) -> ( R gsumg ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( R gsumg ( n e. ( I \ { i } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) )
185	184	oveq1d 6665	. . . . . . . . . . . . . . . . . 18 |- ( y = ( I \ { i } ) -> ( ( R gsumg ( n e. y |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) = ( ( R gsumg ( n e. ( I \ { i } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) )
186	185	ifeq1d 4104	. . . . . . . . . . . . . . . . 17 |- ( y = ( I \ { i } ) -> if ( j = i , ( ( R gsumg ( 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 gsumg ( 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	mpt2eq3dv 6721	. . . . . . . . . . . . . . . 16 |- ( y = ( I \ { i } ) -> ( j e. I , k e. I |-> if ( j = i , ( ( R gsumg ( 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 gsumg ( 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	187	fveq2d 6195	. . . . . . . . . . . . . . 15 |- ( y = ( I \ { i } ) -> ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsumg ( 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 gsumg ( 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	188	eqeq2d 2632	. . . . . . . . . . . . . 14 |- ( y = ( I \ { i } ) -> ( ( ( I maDet R ) ` M ) = ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsumg ( 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 gsumg ( 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 ) ) ) ) ) )
190	182, 189	imbi12d 334	. . . . . . . . . . . . 13 |- ( 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 gsumg ( 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 gsumg ( 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 ) ) ) ) ) ) )
191		fnov 6768	. . . . . . . . . . . . . . . . . 18 |- ( M Fn ( I X. I ) <-> M = ( j e. I , k e. I |-> ( j M k ) ) )
192	60, 191	sylib 208	. . . . . . . . . . . . . . . . 17 |- ( M : ( I X. I ) --> ( Base ` R ) -> M = ( j e. I , k e. I |-> ( j M k ) ) )
193	192	adantl 482	. . . . . . . . . . . . . . . 16 |- ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) -> M = ( j e. I , k e. I |-> ( j M k ) ) )
194		ringgrp 18552	. . . . . . . . . . . . . . . . . 18 |- ( R e. Ring -> R e. Grp )
195	4, 194	syl 17	. . . . . . . . . . . . . . . . 17 |- ( R e. Field -> R e. Grp )
196		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . 22 |- ( i = j -> ( i M k ) = ( j M k ) )
197	196	equcoms 1947	. . . . . . . . . . . . . . . . . . . . 21 |- ( j = i -> ( i M k ) = ( j M k ) )
198	197	oveq2d 6666	. . . . . . . . . . . . . . . . . . . 20 |- ( j = i -> ( ( 0g ` R ) ( +g ` R ) ( i M k ) ) = ( ( 0g ` R ) ( +g ` R ) ( j M k ) ) )
199		simp1l 1085	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( R e. Grp /\ M : ( I X. I ) --> ( Base ` R ) ) /\ j e. I /\ k e. I ) -> R e. Grp )
200		fovrn 6804	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( M : ( I X. I ) --> ( Base ` R ) /\ j e. I /\ k e. I ) -> ( j M k ) e. ( Base ` R ) )
201	200	3adant1l 1318	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( R e. Grp /\ M : ( I X. I ) --> ( Base ` R ) ) /\ j e. I /\ k e. I ) -> ( j M k ) e. ( Base ` R ) )
202		eqid 2622	. . . . . . . . . . . . . . . . . . . . . 22 |- ( +g ` R ) = ( +g ` R )
203	10, 202, 102	grplid 17452	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( R e. Grp /\ ( j M k ) e. ( Base ` R ) ) -> ( ( 0g ` R ) ( +g ` R ) ( j M k ) ) = ( j M k ) )
204	199, 201, 203	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( 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 ) )
205	198, 204	sylan9eqr 2678	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( 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 ) )
206		eqidd 2623	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( R e. Grp /\ M : ( I X. I ) --> ( Base ` R ) ) /\ j e. I /\ k e. I ) /\ -. j = i ) -> ( j M k ) = ( j M k ) )
207	205, 206	ifeqda 4121	. . . . . . . . . . . . . . . . . 18 |- ( ( ( 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 ) )
208	207	mpt2eq3dva 6719	. . . . . . . . . . . . . . . . 17 |- ( ( 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 ) ) )
209	195, 208	sylan 488	. . . . . . . . . . . . . . . 16 |- ( ( 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 ) ) )
210	193, 209	eqtr4d 2659	. . . . . . . . . . . . . . 15 |- ( ( 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 ) ) ) )
211	210	fveq2d 6195	. . . . . . . . . . . . . 14 |- ( ( 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 ) ) ) ) )
212	211	ad4antr 768	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( 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 ) ) ) ) )
213		elun1 3780	. . . . . . . . . . . . . . . . . . . . 21 |- ( i e. x -> i e. ( x u. { z } ) )
214	213	con3i 150	. . . . . . . . . . . . . . . . . . . 20 |- ( -. i e. ( x u. { z } ) -> -. i e. x )
215		ssun1 3776	. . . . . . . . . . . . . . . . . . . . 21 |- x C_ ( x u. { z } )
216		sstr 3611	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( x C_ ( x u. { z } ) /\ ( x u. { z } ) C_ I ) -> x C_ I )
217	215, 216	mpan 706	. . . . . . . . . . . . . . . . . . . 20 |- ( ( x u. { z } ) C_ I -> x C_ I )
218	214, 217	anim12i 590	. . . . . . . . . . . . . . . . . . 19 |- ( ( -. i e. ( x u. { z } ) /\ ( x u. { z } ) C_ I ) -> ( -. i e. x /\ x C_ I ) )
219	218	anim2i 593	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( 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 ) ) )
220	219	adantr 481	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( 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 ) ) )
221		velsn 4193	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( i e. { z } <-> i = z )
222		elun2 3781	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( i e. { z } -> i e. ( x u. { z } ) )
223	221, 222	sylbir 225	. . . . . . . . . . . . . . . . . . . . . 22 |- ( i = z -> i e. ( x u. { z } ) )
224	223	necon3bi 2820	. . . . . . . . . . . . . . . . . . . . 21 |- ( -. i e. ( x u. { z } ) -> i =/= z )
225	224	anim1i 592	. . . . . . . . . . . . . . . . . . . 20 |- ( ( -. i e. ( x u. { z } ) /\ ( x u. { z } ) C_ I ) -> ( i =/= z /\ ( x u. { z } ) C_ I ) )
226		ringcmn 18581	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( R e. Ring -> R e. CMnd )
227	4, 226	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( R e. Field -> R e. CMnd )
228	227	ad7antr 774	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ( ( ( ( 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 )
229		simplr 792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) -> I e. Fin )
230	217	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( i =/= z /\ ( x u. { z } ) C_ I ) -> x C_ I )
231		ssfi 8180	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( I e. Fin /\ x C_ I ) -> x e. Fin )
232	229, 230, 231	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ( 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 )
233	232	ad5ant13 1301	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ( ( ( ( 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 )
234	217	sselda 3603	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( x u. { z } ) C_ I /\ n e. x ) -> n e. I )
235	234	adantll 750	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( i =/= z /\ ( x u. { z } ) C_ I ) /\ n e. x ) -> n e. I )
236	235	ad4ant24 1298	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ( ( ( ( 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 )
237	4	ad6antr 772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ( ( ( 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 )
238	2	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) -> R e. DivRing )
239		ffvelrn 6357	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( ( f : I --> ( Base ` R ) /\ i e. I ) -> ( f ` i ) e. ( Base ` R ) )
240	239	anim2i 593	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( R e. DivRing /\ ( f : I --> ( Base ` R ) /\ i e. I ) ) -> ( R e. DivRing /\ ( f ` i ) e. ( Base ` R ) ) )
241	240	anassrs 680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( R e. DivRing /\ f : I --> ( Base ` R ) ) /\ i e. I ) -> ( R e. DivRing /\ ( f ` i ) e. ( Base ` R ) ) )
242		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 39 |- ( invr ` R ) = ( invr ` R )
243	10, 102, 242	drnginvrcl 18764	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 |- ( ( R e. DivRing /\ ( f ` i ) e. ( Base ` R ) /\ ( f ` i ) =/= ( 0g ` R ) ) -> ( ( invr ` R ) ` ( f ` i ) ) e. ( Base ` R ) )
244	243	3expa 1265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( R e. DivRing /\ ( f ` i ) e. ( Base ` R ) ) /\ ( f ` i ) =/= ( 0g ` R ) ) -> ( ( invr ` R ) ` ( f ` i ) ) e. ( Base ` R ) )
245	241, 244	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( ( R e. DivRing /\ f : I --> ( Base ` R ) ) /\ i e. I ) /\ ( f ` i ) =/= ( 0g ` R ) ) -> ( ( invr ` R ) ` ( f ` i ) ) e. ( Base ` R ) )
246	245	anasss 679	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( R e. DivRing /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) -> ( ( invr ` R ) ` ( f ` i ) ) e. ( Base ` R ) )
247	238, 246	sylanl1 682	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ( 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 ) )
248	247	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ( ( ( 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 ) )
249	44	ad5ant25 1306	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ( ( ( 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 ) )
250		simp-4r 807	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( ( 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 ) )
251	77	3expa 1265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( ( M : ( I X. I ) --> ( Base ` R ) /\ n e. I ) /\ k e. I ) -> ( n M k ) e. ( Base ` R ) )
252	251	an32s 846	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( M : ( I X. I ) --> ( Base ` R ) /\ k e. I ) /\ n e. I ) -> ( n M k ) e. ( Base ` R ) )
253	250, 252	sylanl1 682	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ( ( ( 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 ) )
254	237, 249, 253, 79	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ( ( ( 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 ) )
255	10, 48	ringcl 18561	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( 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 ) )
256	237, 248, 254, 255	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ( ( ( 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 ) )
257	256	adantllr 755	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ( ( ( ( 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 ) )
258	236, 257	syldan 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ( ( ( ( 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 ) )
259	258	adantllr 755	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ( ( ( ( ( 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 ) )
260		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- z e. _V
261	260	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ( ( ( ( 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 )
262		simplr 792	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ( ( ( ( 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 )
263		ssun2 3777	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- { z } C_ ( x u. { z } )
264		sstr 3611	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( { z } C_ ( x u. { z } ) /\ ( x u. { z } ) C_ I ) -> { z } C_ I )
265	263, 264	mpan 706	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( x u. { z } ) C_ I -> { z } C_ I )
266	260	snss 4316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( z e. I <-> { z } C_ I )
267	265, 266	sylibr 224	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( x u. { z } ) C_ I -> z e. I )
268	267	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( i =/= z /\ ( x u. { z } ) C_ I ) -> z e. I )
269	4	ad6antr 772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ( ( ( 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 )
270	4	ad5antr 770	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ( ( 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 )
271	247	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ( ( 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 ) )
272		ffvelrn 6357	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( f : I --> ( Base ` R ) /\ z e. I ) -> ( f ` z ) e. ( Base ` R ) )
273	272	ad4ant24 1298	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ( ( 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 ) )
274	10, 48	ringcl 18561	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( 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 ) )
275	270, 271, 273, 274	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ( ( 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 ) )
276	275	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ( ( ( 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 ) )
277		fovrn 6804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( M : ( I X. I ) --> ( Base ` R ) /\ z e. I /\ k e. I ) -> ( z M k ) e. ( Base ` R ) )
278	277	3expa 1265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( M : ( I X. I ) --> ( Base ` R ) /\ z e. I ) /\ k e. I ) -> ( z M k ) e. ( Base ` R ) )
279	250, 278	sylanl1 682	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ( ( ( 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 ) )
280	10, 48	ringcl 18561	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( 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 ) )
281	269, 276, 279, 280	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ( ( ( 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 ) )
282	268, 281	sylanl2 683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ( ( ( 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 ) )
283	282	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ( ( ( ( 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 ) )
284		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( n = z -> ( f ` n ) = ( f ` z ) )
285		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( n = z -> ( n M k ) = ( z M k ) )
286	284, 285	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( n = z -> ( ( f ` n ) ( .r ` R ) ( n M k ) ) = ( ( f ` z ) ( .r ` R ) ( z M k ) ) )
287	286	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( 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 ) ) ) )
288	247	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ( ( ( 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 ) )
289	272	ad5ant24 1305	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ( ( ( 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 ) )
290	10, 48	ringass 18564	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( 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 ) ) ) )
291	269, 288, 289, 279, 290	syl13anc 1328	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ( ( ( 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 ) ) ) )
292	291	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ( ( ( 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 ) ) )
293	268, 292	sylanl2 683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ( ( ( 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 ) ) )
294	287, 293	sylan9eqr 2678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ( ( ( ( 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 ) ) )
295	294	adantllr 755	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ( ( ( ( ( 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 ) ) )
296	10, 202, 228, 233, 259, 261, 262, 283, 295	gsumunsnd 18357	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ( ( ( ( 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 gsumg ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( ( R gsumg ( 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 ) ) ) )
297	296	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( ( ( ( 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 gsumg ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) = ( ( ( R gsumg ( 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 ) ) )
298		ringabl 18580	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( R e. Ring -> R e. Abel )
299	4, 298	syl 17	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( R e. Field -> R e. Abel )
300	299	ad6antr 772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ( ( ( 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 )
301	227	ad6antr 772	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ( ( ( 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 )
302		vex 3203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- x e. _V
303	302	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ( ( ( 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 )
304		ssel2 3598	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( ( x C_ I /\ n e. x ) -> n e. I )
305	304, 256	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( ( ( ( ( ( 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 ) )
306	305	anassrs 680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( ( ( ( ( ( ( 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 ) )
307		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( 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 ) ) ) )
308	306, 307	fmptd 6385	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( ( ( ( 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 ) )
309	308	an32s 846	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ( ( ( 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 ) )
310		ovex 6678	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 |- ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) e. _V
311	310, 307	fnmpti 6022	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 |- ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) Fn x
312	311	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( I e. Fin /\ x C_ I ) -> ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) Fn x )
313		fvexd 6203	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 35 |- ( ( I e. Fin /\ x C_ I ) -> ( 0g ` R ) e. _V )
314	312, 231, 313	fndmfifsupp 8288	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 |- ( ( 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 ) )
315	314	adantll 750	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( 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 ) )
316	315	ad5ant14 1302	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ( ( ( 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 ) )
317	10, 102, 301, 303, 309, 316	gsumcl 18316	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ( ( ( 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 gsumg ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) e. ( Base ` R ) )
318	217, 317	sylanl2 683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ( ( ( 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 gsumg ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) e. ( Base ` R ) )
319	267, 281	sylanl2 683	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ( ( ( 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 ) )
320		simpllr 799	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) -> M : ( I X. I ) --> ( Base ` R ) )
321		simpl 473	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 |- ( ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) -> i e. I )
322	320, 321	anim12i 590	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( ( ( ( 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 ) )
323	322	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( ( ( ( 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 ) )
324		fovrn 6804	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( ( M : ( I X. I ) --> ( Base ` R ) /\ i e. I /\ k e. I ) -> ( i M k ) e. ( Base ` R ) )
325	324	3expa 1265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( ( M : ( I X. I ) --> ( Base ` R ) /\ i e. I ) /\ k e. I ) -> ( i M k ) e. ( Base ` R ) )
326	323, 325	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( ( ( ( ( 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 ) )
327	10, 202, 300, 318, 319, 326	abl32 18214	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( ( ( ( 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 gsumg ( 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 gsumg ( 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	327	adantlrl 756	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( ( ( ( ( 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 gsumg ( 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 gsumg ( 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	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( ( ( ( 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 gsumg ( 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 gsumg ( 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 ) ) ) )
330	297, 329	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( ( ( ( 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 gsumg ( n e. ( x u. { z } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) = ( ( ( R gsumg ( 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 ) ) ) )
331	330	ifeq1d 4104	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( ( ( 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 gsumg ( 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 gsumg ( 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	3adant2 1080	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ( ( ( 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 gsumg ( 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 gsumg ( 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	332	mpt2eq3dva 6719	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ( ( 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 gsumg ( 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 gsumg ( 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 ) ) ) ) )
334	333	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ( ( 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 gsumg ( 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 gsumg ( 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 ) ) ) ) ) )
335		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( I maDet R ) = ( I maDet R )
336	1	simprbi 480	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( R e. Field -> R e. CRing )
337	336	ad5antr 770	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ( 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 )
338		simp-4r 807	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ( 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 )
339	195	ad6antr 772	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( ( ( 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 )
340	322	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( ( 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 ) )
341	340, 325	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( ( ( 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 ) )
342	10, 202	grpcl 17430	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( R e. Grp /\ ( R gsumg ( 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 gsumg ( 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	339, 317, 341, 342	syl3anc 1326	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( ( 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 gsumg ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) e. ( Base ` R ) )
344	230, 343	sylanl2 683	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ( ( 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 gsumg ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) e. ( Base ` R ) )
345	250, 268	anim12i 590	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( 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 ) )
346	345, 278	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ( ( 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 ) )
347		simp-5r 809	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( 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 ) )
348	347, 200	syl3an1 1359	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ( ( 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 ) )
349	268, 275	sylan2 491	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ( 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 ) )
350		simplrl 800	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ( 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 )
351	267	ad2antll 765	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ( 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 )
352		simprl 794	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ( 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 )
353	335, 10, 202, 48, 337, 338, 344, 346, 348, 349, 350, 351, 352	mdetero 20416	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ( 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 gsumg ( 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 gsumg ( 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	353	adantr 481	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ( ( 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 gsumg ( 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 gsumg ( 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 ) ) ) ) ) )
355	334, 354	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ( ( 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 gsumg ( 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 gsumg ( 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 ) ) ) ) ) )
356		iftrue 4092	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( j = z -> if ( j = z , ( z M k ) , ( j M k ) ) = ( z M k ) )
357		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( j = z -> ( j M k ) = ( z M k ) )
358	356, 357	eqtr4d 2659	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( j = z -> if ( j = z , ( z M k ) , ( j M k ) ) = ( j M k ) )
359		iffalse 4095	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( -. j = z -> if ( j = z , ( z M k ) , ( j M k ) ) = ( j M k ) )
360	358, 359	pm2.61i 176	. . . . . . . . . . . . . . . . . . . . . . . 24 |- if ( j = z , ( z M k ) , ( j M k ) ) = ( j M k )
361		ifeq2 4091	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( if ( j = z , ( z M k ) , ( j M k ) ) = ( j M k ) -> if ( j = i , ( ( R gsumg ( 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 gsumg ( 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	360, 361	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( j e. I /\ k e. I ) -> if ( j = i , ( ( R gsumg ( 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 gsumg ( 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	362	mpt2eq3ia 6720	. . . . . . . . . . . . . . . . . . . . . 22 |- ( j e. I , k e. I |-> if ( j = i , ( ( R gsumg ( 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 gsumg ( 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 ) ) )
364	363	fveq2i 6194	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsumg ( 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 gsumg ( 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 ) ) ) )
365		ifeq2 4091	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( if ( j = z , ( z M k ) , ( j M k ) ) = ( j M k ) -> if ( j = i , ( ( R gsumg ( 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 gsumg ( 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	360, 365	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( j e. I /\ k e. I ) -> if ( j = i , ( ( R gsumg ( 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 gsumg ( 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	366	mpt2eq3ia 6720	. . . . . . . . . . . . . . . . . . . . . 22 |- ( j e. I , k e. I |-> if ( j = i , ( ( R gsumg ( 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 gsumg ( 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	367	fveq2i 6194	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( I maDet R ) ` ( j e. I , k e. I |-> if ( j = i , ( ( R gsumg ( 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 gsumg ( 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	355, 364, 368	3eqtr3g 2679	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ( 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 gsumg ( 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 gsumg ( 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	225, 369	sylanl2 683	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( 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 gsumg ( 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 gsumg ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) )
371	370	eqeq2d 2632	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( 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 gsumg ( 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 gsumg ( n e. x |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) , ( j M k ) ) ) ) ) )
372	371	biimprd 238	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( ( 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 gsumg ( 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 gsumg ( 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	220, 372	embantd 59	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( ( ( 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 gsumg ( 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 gsumg ( 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	expcom 451	. . . . . . . . . . . . . . 15 |- ( -. 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 gsumg ( 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 gsumg ( 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	374	com23 86	. . . . . . . . . . . . . 14 |- ( -. 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 gsumg ( 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 gsumg ( 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 ) ) ) ) ) ) )
376	375	adantl 482	. . . . . . . . . . . . 13 |- ( ( 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 gsumg ( 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 gsumg ( 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 ) ) ) ) ) ) )
377	151, 164, 177, 190, 212, 376	findcard2s 8201	. . . . . . . . . . . 12 |- ( ( 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 gsumg ( 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	134, 377	mpcom 38	. . . . . . . . . . 11 |- ( ( ( ( ( ( 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 gsumg ( 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	131, 132, 378	mpanr12 721	. . . . . . . . . 10 |- ( ( ( ( ( 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 gsumg ( 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 ) ) ) ) )
380	379	adantlr 751	. . . . . . . . 9 |- ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( k e. I |-> ( R gsumg ( 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 gsumg ( 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 ) ) ) ) )
381		eqid 2622	. . . . . . . . . . . 12 |- I = I
382		fconstmpt 5163	. . . . . . . . . . . . . . . . 17 |- ( I X. { ( 0g ` R ) } ) = ( k e. I |-> ( 0g ` R ) )
383	382	eqeq2i 2634	. . . . . . . . . . . . . . . 16 |- ( ( k e. I |-> ( R gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) <-> ( k e. I |-> ( R gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( k e. I |-> ( 0g ` R ) ) )
384		ovex 6678	. . . . . . . . . . . . . . . . . 18 |- ( R gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) e. _V
385	384	rgenw 2924	. . . . . . . . . . . . . . . . 17 |- A. k e. I ( R gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) e. _V
386		mpteqb 6299	. . . . . . . . . . . . . . . . 17 |- ( A. k e. I ( R gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) e. _V -> ( ( k e. I |-> ( R gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( k e. I |-> ( 0g ` R ) ) <-> A. k e. I ( R gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) = ( 0g ` R ) ) )
387	385, 386	ax-mp 5	. . . . . . . . . . . . . . . 16 |- ( ( k e. I |-> ( R gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( k e. I |-> ( 0g ` R ) ) <-> A. k e. I ( R gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) = ( 0g ` R ) )
388	383, 387	bitri 264	. . . . . . . . . . . . . . 15 |- ( ( k e. I |-> ( R gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) <-> A. k e. I ( R gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) = ( 0g ` R ) )
389	227	ad5antr 770	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ( 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 )
390		simp-4r 807	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ( 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 )
391		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( 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 ) ) ) )
392	310, 391	fnmpti 6022	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( n e. I |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) Fn I
393	392	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( I e. Fin -> ( n e. I |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) Fn I )
394		id 22	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( I e. Fin -> I e. Fin )
395		fvexd 6203	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( I e. Fin -> ( 0g ` R ) e. _V )
396	393, 394, 395	fndmfifsupp 8288	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( I e. Fin -> ( n e. I |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) finSupp ( 0g ` R ) )
397	396	ad4antlr 769	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ( 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 ) )
398		simplrl 800	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ( 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 )
399	322, 325	sylan 488	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ( 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 ) )
400		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( n = i -> ( f ` n ) = ( f ` i ) )
401		oveq1 6657	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( n = i -> ( n M k ) = ( i M k ) )
402	400, 401	oveq12d 6668	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( n = i -> ( ( f ` n ) ( .r ` R ) ( n M k ) ) = ( ( f ` i ) ( .r ` R ) ( i M k ) ) )
403	402	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( 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 ) ) ) )
404		simpll 790	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) -> R e. Field )
405	2, 239	anim12i 590	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( R e. Field /\ ( f : I --> ( Base ` R ) /\ i e. I ) ) -> ( R e. DivRing /\ ( f ` i ) e. ( Base ` R ) ) )
406	405	anassrs 680	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( R e. Field /\ f : I --> ( Base ` R ) ) /\ i e. I ) -> ( R e. DivRing /\ ( f ` i ) e. ( Base ` R ) ) )
407		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 |- ( 1r ` R ) = ( 1r ` R )
408	10, 102, 48, 407, 242	drnginvrl 18766	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 |- ( ( R e. DivRing /\ ( f ` i ) e. ( Base ` R ) /\ ( f ` i ) =/= ( 0g ` R ) ) -> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` i ) ) = ( 1r ` R ) )
409	408	3expa 1265	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 |- ( ( ( R e. DivRing /\ ( f ` i ) e. ( Base ` R ) ) /\ ( f ` i ) =/= ( 0g ` R ) ) -> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` i ) ) = ( 1r ` R ) )
410	406, 409	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( ( ( R e. Field /\ f : I --> ( Base ` R ) ) /\ i e. I ) /\ ( f ` i ) =/= ( 0g ` R ) ) -> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` i ) ) = ( 1r ` R ) )
411	410	anasss 679	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( R e. Field /\ f : I --> ( Base ` R ) ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) -> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( f ` i ) ) = ( 1r ` R ) )
412	411	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( 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 ) ) )
413	404, 412	sylanl1 682	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( 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 ) ) )
414	413	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( 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 ) ) )
415	4	ad5antr 770	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( ( 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 )
416	247	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( ( 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 ) )
417	239	ad2ant2lr 784	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( ( ( 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 ) )
418	417	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( ( 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 ) )
419	10, 48	ringass 18564	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( 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 ) ) ) )
420	415, 416, 418, 399, 419	syl13anc 1328	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( 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 ) ) ) )
421	4	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 |- ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) -> R e. Ring )
422	421	3ad2ant1 1082	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ i e. I /\ k e. I ) -> R e. Ring )
423	324	3adant1l 1318	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ i e. I /\ k e. I ) -> ( i M k ) e. ( Base ` R ) )
424	10, 48, 407	ringlidm 18571	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 |- ( ( R e. Ring /\ ( i M k ) e. ( Base ` R ) ) -> ( ( 1r ` R ) ( .r ` R ) ( i M k ) ) = ( i M k ) )
425	422, 423, 424	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( ( 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 ) )
426	425	ad5ant145 1315	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( ( ( ( ( ( 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 ) )
427	426	adantlrr 757	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( ( ( ( ( ( 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 ) )
428	414, 420, 427	3eqtr3d 2664	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( ( ( ( ( ( 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 ) )
429	403, 428	sylan9eqr 2678	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ( ( 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 ) )
430	10, 202, 389, 390, 397, 256, 398, 399, 429	gsumdifsnd 18360	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ( 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 gsumg ( n e. I |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( ( R gsumg ( n e. ( I \ { i } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) )
431		ovex 6678	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( ( f ` n ) ( .r ` R ) ( n M k ) ) e. _V
432		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 |- ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) = ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) )
433	431, 432	fnmpti 6022	. . . . . . . . . . . . . . . . . . . . . . . . . 26 |- ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) Fn I
434	433	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . 25 |- ( I e. Fin -> ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) Fn I )
435	434, 394, 395	fndmfifsupp 8288	. . . . . . . . . . . . . . . . . . . . . . . 24 |- ( I e. Fin -> ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) finSupp ( 0g ` R ) )
436	435	ad4antlr 769	. . . . . . . . . . . . . . . . . . . . . . 23 |- ( ( ( ( ( ( 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 ) )
437	10, 102, 202, 48, 415, 390, 416, 254, 436	gsummulc2 18607	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( ( 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 gsumg ( n e. I |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( R gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) )
438	430, 437	eqtr3d 2658	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( ( 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 gsumg ( 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 gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) )
439	438	adantr 481	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ( 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 gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) = ( 0g ` R ) ) -> ( ( R gsumg ( 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 gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) )
440		oveq2 6658	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( R gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) = ( 0g ` R ) -> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( R gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( 0g ` R ) ) )
441	440	adantl 482	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ( 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 gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) = ( 0g ` R ) ) -> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( R gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( 0g ` R ) ) )
442	4	ad4antr 768	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( ( ( ( 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 )
443	10, 48, 102	ringrz 18588	. . . . . . . . . . . . . . . . . . . . . 22 |- ( ( R e. Ring /\ ( ( invr ` R ) ` ( f ` i ) ) e. ( Base ` R ) ) -> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
444	442, 247, 443	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 |- ( ( ( ( ( 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 ) )
445	444	ad2antrr 762	. . . . . . . . . . . . . . . . . . . 20 |- ( ( ( ( ( ( ( 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 gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) = ( 0g ` R ) ) -> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( 0g ` R ) ) = ( 0g ` R ) )
446	439, 441, 445	3eqtrd 2660	. . . . . . . . . . . . . . . . . . 19 |- ( ( ( ( ( ( ( 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 gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) = ( 0g ` R ) ) -> ( ( R gsumg ( n e. ( I \ { i } ) |-> ( ( ( invr ` R ) ` ( f ` i ) ) ( .r ` R ) ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) ( +g ` R ) ( i M k ) ) = ( 0g ` R ) )
447	446	ifeq1d 4104	. . . . . . . . . . . . . . . . . 18 |- ( ( ( ( ( ( ( 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 gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) = ( 0g ` R ) ) -> if ( j = i , ( ( R gsumg ( 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	ex 450	. . . . . . . . . . . . . . . . 17 |- ( ( ( ( ( ( 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 gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) = ( 0g ` R ) -> if ( j = i , ( ( R gsumg ( 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	448	ralimdva 2962	. . . . . . . . . . . . . . . 16 |- ( ( ( ( ( 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 gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) = ( 0g ` R ) -> A. k e. I if ( j = i , ( ( R gsumg ( 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	imp 445	. . . . . . . . . . . . . . 15 |- ( ( ( ( ( ( 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 gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) = ( 0g ` R ) ) -> A. k e. I if ( j = i , ( ( R gsumg ( 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	388, 450	sylan2b 492	. . . . . . . . . . . . . 14 |- ( ( ( ( ( ( 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 gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) ) -> A. k e. I if ( j = i , ( ( R gsumg ( 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	451, 381	jctil 560	. . . . . . . . . . . . 13 |- ( ( ( ( ( ( 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 gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) ) -> ( I = I /\ A. k e. I if ( j = i , ( ( R gsumg ( 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 ) ) ) )
453	452	ralrimivw 2967	. . . . . . . . . . . 12 |- ( ( ( ( ( ( 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 gsumg ( 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 gsumg ( 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 ) ) ) )
454		mpt2eq123 6714	. . . . . . . . . . . 12 |- ( ( I = I /\ A. j e. I ( I = I /\ A. k e. I if ( j = i , ( ( R gsumg ( 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 gsumg ( 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	381, 453, 454	sylancr 695	. . . . . . . . . . 11 |- ( ( ( ( ( ( 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 gsumg ( n e. I |-> ( ( f ` n ) ( .r ` R ) ( n M k ) ) ) ) ) = ( I X. { ( 0g ` R ) } ) ) -> ( j e. I , k e. I |-> if ( j = i , ( ( R gsumg ( 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 ) ) ) )
456	455	an32s 846	. . . . . . . . . 10 |- ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( k e. I |-> ( R gsumg ( 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 gsumg ( 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 ) ) ) )
457	456	fveq2d 6195	. . . . . . . . 9 |- ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( k e. I |-> ( R gsumg ( 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 gsumg ( 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 ) ) ) ) )
458	336	ad3antrrr 766	. . . . . . . . . . 11 |- ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) -> R e. CRing )
459		simplr 792	. . . . . . . . . . 11 |- ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) -> I e. Fin )
460		simpllr 799	. . . . . . . . . . . 12 |- ( ( ( ( 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 ) )
461	460, 200	syl3an1 1359	. . . . . . . . . . 11 |- ( ( ( ( ( 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 ) )
462		simprl 794	. . . . . . . . . . 11 |- ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ ( i e. I /\ ( f ` i ) =/= ( 0g ` R ) ) ) -> i e. I )
463	335, 10, 102, 458, 459, 461, 462	mdetr0 20411	. . . . . . . . . 10 |- ( ( ( ( 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 ) )
464	463	ad4ant14 1293	. . . . . . . . 9 |- ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( k e. I |-> ( R gsumg ( 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 ) )
465	380, 457, 464	3eqtrd 2660	. . . . . . . 8 |- ( ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( k e. I |-> ( R gsumg ( 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 ) )
466	465	rexlimdvaa 3032	. . . . . . 7 |- ( ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) /\ ( k e. I |-> ( R gsumg ( 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 ) ) )
467	466	expimpd 629	. . . . . 6 |- ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) -> ( ( ( k e. I |-> ( R gsumg ( 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 ) ) )
468	130, 467	sylan2d 499	. . . . 5 |- ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f : I --> ( Base ` R ) ) -> ( ( ( k e. I |-> ( R gsumg ( 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	33, 468	sylan2 491	. . . 4 |- ( ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) /\ f e. ( ( Base ` R ) ^m I ) ) -> ( ( ( k e. I |-> ( R gsumg ( 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	469	rexlimdva 3031	. . 3 |- ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. Fin ) -> ( E. f e. ( ( Base ` R ) ^m I ) ( ( k e. I |-> ( R gsumg ( 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 ) ) )
471	9, 470	sylan2 491	. 2 |- ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) -> ( E. f e. ( ( Base ` R ) ^m I ) ( ( k e. I |-> ( R gsumg ( 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 ) ) )
472	117, 471	sylbid 230	1 |- ( ( ( R e. Field /\ M : ( I X. I ) --> ( Base ` R ) ) /\ I e. ( Fin \ { (/) } ) ) -> ( -. curry M LIndF ( R freeLMod I ) -> ( ( I maDet R ) ` M ) = ( 0g ` R ) ) )

Syntax hints:   -. wn 3   -> wi 4   <-> wb 196   /\ wa 384   /\ w3a 1037   = wceq 1483   e. wcel 1990   =/= wne 2794   A.wral 2912   E.wrex 2913   _Vcvv 3200   \ cdif 3571   u. cun 3572   C_ wss 3574   (/)c0 3915   ifcif 4086   {csn 4177   class class class wbr 4653   |-> cmpt 4729   X. cxp 5112   Fn wfn 5883   -->wf 5884   ` cfv 5888  (class class class)co 6650   |-> cmpt2 6652   oFcof 6895  curry ccur 7391   ^m cmap 7857   Fincfn 7955   finSupp cfsupp 8275   Basecbs 15857   +g cplusg 15941   .rcmulr 15942  Scalarcsca 15944   .scvsca 15945   0gc0g 16100   gsum_g cgsu 16101   Grpcgrp 17422  CMndccmn 18193   Abelcabl 18194   1rcur 18501   Ringcrg 18547   CRingccrg 18548   invrcinvr 18671   DivRingcdr 18747  Fieldcfield 18748   LModclmod 18863   freeLMod cfrlm 20090   LIndF clindf 20143   maDet cmdat 20390

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-8 1992  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-rep 4771  ax-sep 4781  ax-nul 4789  ax-pow 4843  ax-pr 4906  ax-un 6949  ax-inf2 8538  ax-cnex 9992  ax-resscn 9993  ax-1cn 9994  ax-icn 9995  ax-addcl 9996  ax-addrcl 9997  ax-mulcl 9998  ax-mulrcl 9999  ax-mulcom 10000  ax-addass 10001  ax-mulass 10002  ax-distr 10003  ax-i2m1 10004  ax-1ne0 10005  ax-1rid 10006  ax-rnegex 10007  ax-rrecex 10008  ax-cnre 10009  ax-pre-lttri 10010  ax-pre-lttrn 10011  ax-pre-ltadd 10012  ax-pre-mulgt0 10013  ax-addf 10015  ax-mulf 10016

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1038  df-3an 1039  df-xor 1465  df-tru 1486  df-fal 1489  df-ex 1705  df-nf 1710  df-sb 1881  df-eu 2474  df-mo 2475  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ne 2795  df-nel 2898  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3202  df-sbc 3436  df-csb 3534  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-pss 3590  df-nul 3916  df-if 4087  df-pw 4160  df-sn 4178  df-pr 4180  df-tp 4182  df-op 4184  df-ot 4186  df-uni 4437  df-int 4476  df-iun 4522  df-iin 4523  df-br 4654  df-opab 4713  df-mpt 4730  df-tr 4753  df-id 5024  df-eprel 5029  df-po 5035  df-so 5036  df-fr 5073  df-se 5074  df-we 5075  df-xp 5120  df-rel 5121  df-cnv 5122  df-co 5123  df-dm 5124  df-rn 5125  df-res 5126  df-ima 5127  df-pred 5680  df-ord 5726  df-on 5727  df-lim 5728  df-suc 5729  df-iota 5851  df-fun 5890  df-fn 5891  df-f 5892  df-f1 5893  df-fo 5894  df-f1o 5895  df-fv 5896  df-isom 5897  df-riota 6611  df-ov 6653  df-oprab 6654  df-mpt2 6655  df-of 6897  df-om 7066  df-1st 7168  df-2nd 7169  df-supp 7296  df-tpos 7352  df-cur 7393  df-wrecs 7407  df-recs 7468  df-rdg 7506  df-1o 7560  df-2o 7561  df-oadd 7564  df-er 7742  df-map 7859  df-pm 7860  df-ixp 7909  df-en 7956  df-dom 7957  df-sdom 7958  df-fin 7959  df-fsupp 8276  df-sup 8348  df-oi 8415  df-card 8765  df-pnf 10076  df-mnf 10077  df-xr 10078  df-ltxr 10079  df-le 10080  df-sub 10268  df-neg 10269  df-div 10685  df-nn 11021  df-2 11079  df-3 11080  df-4 11081  df-5 11082  df-6 11083  df-7 11084  df-8 11085  df-9 11086  df-n0 11293  df-xnn0 11364  df-z 11378  df-dec 11494  df-uz 11688  df-rp 11833  df-fz 12327  df-fzo 12466  df-seq 12802  df-exp 12861  df-hash 13118  df-word 13299  df-lsw 13300  df-concat 13301  df-s1 13302  df-substr 13303  df-splice 13304  df-reverse 13305  df-s2 13593  df-struct 15859  df-ndx 15860  df-slot 15861  df-base 15863  df-sets 15864  df-ress 15865  df-plusg 15954  df-mulr 15955  df-starv 15956  df-sca 15957  df-vsca 15958  df-ip 15959  df-tset 15960  df-ple 15961  df-ds 15964  df-unif 15965  df-hom 15966  df-cco 15967  df-0g 16102  df-gsum 16103  df-prds 16108  df-pws 16110  df-mre 16246  df-mrc 16247  df-acs 16249  df-mgm 17242  df-sgrp 17284  df-mnd 17295  df-mhm 17335  df-submnd 17336  df-grp 17425  df-minusg 17426  df-sbg 17427  df-mulg 17541  df-subg 17591  df-ghm 17658  df-gim 17701  df-cntz 17750  df-oppg 17776  df-symg 17798  df-pmtr 17862  df-psgn 17911  df-evpm 17912  df-cmn 18195  df-abl 18196  df-mgp 18490  df-ur 18502  df-ring 18549  df-cring 18550  df-oppr 18623  df-dvdsr 18641  df-unit 18642  df-invr 18672  df-dvr 18683  df-rnghom 18715  df-drng 18749  df-field 18750  df-subrg 18778  df-lmod 18865  df-lss 18933  df-lsp 18972  df-lmhm 19022  df-lbs 19075  df-sra 19172  df-rgmod 19173  df-nzr 19258  df-cnfld 19747  df-zring 19819  df-zrh 19852  df-dsmm 20076  df-frlm 20091  df-uvc 20122  df-lindf 20145  df-mat 20214  df-mdet 20391

This theorem is referenced by:  matunitlindf  33407