# Metamath Proof Explorer

## Theorem matunitlindflem2

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

Ref Expression
Assertion matunitlindflem2 ${⊢}\left(\left(\left({R}\in \mathrm{Field}\wedge {M}\in {\mathrm{Base}}_{\left({I}\mathrm{Mat}{R}\right)}\right)\wedge {I}\ne \varnothing \right)\wedge curry{M}\mathrm{LIndF}\left({R}\mathrm{freeLMod}{I}\right)\right)\to \left({I}\mathrm{maDet}{R}\right)\left({M}\right)\in \mathrm{Unit}\left({R}\right)$

### Proof

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