matunitlindflem1

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

Proof

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

Metamath Proof Explorer

Theorem matunitlindflem1

Proof