matunitlindflem2

		Ref	Expression
	Assertion	matunitlindflem2	$⊢ (((R \in Field \land M \in {Base}_{(I Mat R)}) \land I \neq \emptyset) \land curry M LIndF (R freeLMod I)) \to (I maDet R) (M) \in Unit (R)$

Proof

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

Metamath Proof Explorer

Theorem matunitlindflem2

Proof