Metamath Proof Explorer

Theorem matunitlindflem2

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

Ref Expression
Assertion matunitlindflem2 ( ( ( ( 𝑅 ∈ Field ∧ 𝑀 ∈ ( Base ‘ ( 𝐼 Mat 𝑅 ) ) ) ∧ 𝐼 ≠ ∅ ) ∧ curry 𝑀 LIndF ( 𝑅 freeLMod 𝐼 ) ) → ( ( 𝐼 maDet 𝑅 ) ‘ 𝑀 ) ∈ ( Unit ‘ 𝑅 ) )

Proof

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