matunitlindflem1

		Ref	Expression
	Assertion	matunitlindflem1	$⊢ ((R \in Field \land M : I \times I ⟶ {Base}_{R}) \land I \in (Fin ∖ \{\emptyset\})) \to (\neg curry M LIndF (R freeLMod I) \to (I maDet R) (M) = 0_{R})$

Proof

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

Metamath Proof Explorer

Theorem matunitlindflem1

Proof