Metamath Proof Explorer

Theorem matunitlindf

Description: A matrix over a field is invertible iff the rows are linearly independent. (Contributed by Brendan Leahy, 2-Jun-2021)

Ref Expression
Assertion matunitlindf ( ( 𝑅 ∈ Field ∧ 𝑀 ∈ ( Base ‘ ( 𝐼 Mat 𝑅 ) ) ) → ( 𝑀 ∈ ( Unit ‘ ( 𝐼 Mat 𝑅 ) ) ↔ curry 𝑀 LIndF ( 𝑅 freeLMod 𝐼 ) ) )

Proof

Step Hyp Ref Expression
1 fvoveq1 ⊢ ( 𝐼 = ∅ → ( Base ‘ ( 𝐼 Mat 𝑅 ) ) = ( Base ‘ ( ∅ Mat 𝑅 ) ) )
2 mat0dimbas0 ⊢ ( 𝑅 ∈ Field → ( Base ‘ ( ∅ Mat 𝑅 ) ) = { ∅ } )
3 1 2 sylan9eq ⊢ ( ( 𝐼 = ∅ ∧ 𝑅 ∈ Field ) → ( Base ‘ ( 𝐼 Mat 𝑅 ) ) = { ∅ } )
4 3 eleq2d ⊢ ( ( 𝐼 = ∅ ∧ 𝑅 ∈ Field ) → ( 𝑀 ∈ ( Base ‘ ( 𝐼 Mat 𝑅 ) ) ↔ 𝑀 ∈ { ∅ } ) )
5 elsni ⊢ ( 𝑀 ∈ { ∅ } → 𝑀 = ∅ )
6 4 5 syl6bi ⊢ ( ( 𝐼 = ∅ ∧ 𝑅 ∈ Field ) → ( 𝑀 ∈ ( Base ‘ ( 𝐼 Mat 𝑅 ) ) → 𝑀 = ∅ ) )
7 6 imdistanda ⊢ ( 𝐼 = ∅ → ( ( 𝑅 ∈ Field ∧ 𝑀 ∈ ( Base ‘ ( 𝐼 Mat 𝑅 ) ) ) → ( 𝑅 ∈ Field ∧ 𝑀 = ∅ ) ) )
8 7 impcom ⊢ ( ( ( 𝑅 ∈ Field ∧ 𝑀 ∈ ( Base ‘ ( 𝐼 Mat 𝑅 ) ) ) ∧ 𝐼 = ∅ ) → ( 𝑅 ∈ Field ∧ 𝑀 = ∅ ) )
9 isfld ⊢ ( 𝑅 ∈ Field ↔ ( 𝑅 ∈ DivRing ∧ 𝑅 ∈ CRing ) )
10 9 simplbi ⊢ ( 𝑅 ∈ Field → 𝑅 ∈ DivRing )
11 drngring ⊢ ( 𝑅 ∈ DivRing → 𝑅 ∈ Ring )
12 eqid ⊢ ( ∅ Mat 𝑅 ) = ( ∅ Mat 𝑅 )
13 12 mat0dimid ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ ( ∅ Mat 𝑅 ) ) = ∅ )
14 0fin ⊢ ∅ ∈ Fin
15 12 matring ⊢ ( ( ∅ ∈ Fin ∧ 𝑅 ∈ Ring ) → ( ∅ Mat 𝑅 ) ∈ Ring )
16 14 15 mpan ⊢ ( 𝑅 ∈ Ring → ( ∅ Mat 𝑅 ) ∈ Ring )
17 eqid ⊢ ( Unit ‘ ( ∅ Mat 𝑅 ) ) = ( Unit ‘ ( ∅ Mat 𝑅 ) )
18 eqid ⊢ ( 1r ‘ ( ∅ Mat 𝑅 ) ) = ( 1r ‘ ( ∅ Mat 𝑅 ) )
19 17 18 1unit ⊢ ( ( ∅ Mat 𝑅 ) ∈ Ring → ( 1r ‘ ( ∅ Mat 𝑅 ) ) ∈ ( Unit ‘ ( ∅ Mat 𝑅 ) ) )
20 16 19 syl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ ( ∅ Mat 𝑅 ) ) ∈ ( Unit ‘ ( ∅ Mat 𝑅 ) ) )
21 13 20 eqeltrrd ⊢ ( 𝑅 ∈ Ring → ∅ ∈ ( Unit ‘ ( ∅ Mat 𝑅 ) ) )
22 10 11 21 3syl ⊢ ( 𝑅 ∈ Field → ∅ ∈ ( Unit ‘ ( ∅ Mat 𝑅 ) ) )
23 f0 ⊢ ∅ : ∅ ⟶ ( Base ‘ ( 𝑅 freeLMod ∅ ) )
24 dm0 ⊢ dom ∅ = ∅
25 24 feq2i ⊢ ( ∅ : dom ∅ ⟶ ( Base ‘ ( 𝑅 freeLMod ∅ ) ) ↔ ∅ : ∅ ⟶ ( Base ‘ ( 𝑅 freeLMod ∅ ) ) )
26 23 25 mpbir ⊢ ∅ : dom ∅ ⟶ ( Base ‘ ( 𝑅 freeLMod ∅ ) )
27 rzal ⊢ ( dom ∅ = ∅ → ∀ 𝑥 ∈ dom ∅ ∀ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod ∅ ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod ∅ ) ) ) } ) ¬ ( 𝑦 ( ·𝑠 ‘ ( 𝑅 freeLMod ∅ ) ) ( ∅ ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ ( 𝑅 freeLMod ∅ ) ) ‘ ( ∅ “ ( dom ∅ ∖ { 𝑥 } ) ) ) )
28 24 27 ax-mp ⊢ ∀ 𝑥 ∈ dom ∅ ∀ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod ∅ ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod ∅ ) ) ) } ) ¬ ( 𝑦 ( ·𝑠 ‘ ( 𝑅 freeLMod ∅ ) ) ( ∅ ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ ( 𝑅 freeLMod ∅ ) ) ‘ ( ∅ “ ( dom ∅ ∖ { 𝑥 } ) ) )
29 ovex ⊢ ( 𝑅 freeLMod ∅ ) ∈ V
30 eqid ⊢ ( Base ‘ ( 𝑅 freeLMod ∅ ) ) = ( Base ‘ ( 𝑅 freeLMod ∅ ) )
31 eqid ⊢ ( ·𝑠 ‘ ( 𝑅 freeLMod ∅ ) ) = ( ·𝑠 ‘ ( 𝑅 freeLMod ∅ ) )
32 eqid ⊢ ( LSpan ‘ ( 𝑅 freeLMod ∅ ) ) = ( LSpan ‘ ( 𝑅 freeLMod ∅ ) )
33 eqid ⊢ ( Scalar ‘ ( 𝑅 freeLMod ∅ ) ) = ( Scalar ‘ ( 𝑅 freeLMod ∅ ) )
34 eqid ⊢ ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod ∅ ) ) ) = ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod ∅ ) ) )
35 eqid ⊢ ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod ∅ ) ) ) = ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod ∅ ) ) )
36 30 31 32 33 34 35 islindf ⊢ ( ( ( 𝑅 freeLMod ∅ ) ∈ V ∧ ∅ ∈ Fin ) → ( ∅ LIndF ( 𝑅 freeLMod ∅ ) ↔ ( ∅ : dom ∅ ⟶ ( Base ‘ ( 𝑅 freeLMod ∅ ) ) ∧ ∀ 𝑥 ∈ dom ∅ ∀ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod ∅ ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod ∅ ) ) ) } ) ¬ ( 𝑦 ( ·𝑠 ‘ ( 𝑅 freeLMod ∅ ) ) ( ∅ ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ ( 𝑅 freeLMod ∅ ) ) ‘ ( ∅ “ ( dom ∅ ∖ { 𝑥 } ) ) ) ) ) )
37 29 14 36 mp2an ⊢ ( ∅ LIndF ( 𝑅 freeLMod ∅ ) ↔ ( ∅ : dom ∅ ⟶ ( Base ‘ ( 𝑅 freeLMod ∅ ) ) ∧ ∀ 𝑥 ∈ dom ∅ ∀ 𝑦 ∈ ( ( Base ‘ ( Scalar ‘ ( 𝑅 freeLMod ∅ ) ) ) ∖ { ( 0g ‘ ( Scalar ‘ ( 𝑅 freeLMod ∅ ) ) ) } ) ¬ ( 𝑦 ( ·𝑠 ‘ ( 𝑅 freeLMod ∅ ) ) ( ∅ ‘ 𝑥 ) ) ∈ ( ( LSpan ‘ ( 𝑅 freeLMod ∅ ) ) ‘ ( ∅ “ ( dom ∅ ∖ { 𝑥 } ) ) ) ) )
38 26 28 37 mpbir2an ⊢ ∅ LIndF ( 𝑅 freeLMod ∅ )
39 38 a1i ⊢ ( 𝑅 ∈ Field → ∅ LIndF ( 𝑅 freeLMod ∅ ) )
40 22 39 2thd ⊢ ( 𝑅 ∈ Field → ( ∅ ∈ ( Unit ‘ ( ∅ Mat 𝑅 ) ) ↔ ∅ LIndF ( 𝑅 freeLMod ∅ ) ) )
41 fvoveq1 ⊢ ( 𝐼 = ∅ → ( Unit ‘ ( 𝐼 Mat 𝑅 ) ) = ( Unit ‘ ( ∅ Mat 𝑅 ) ) )
42 eleq12 ⊢ ( ( 𝑀 = ∅ ∧ ( Unit ‘ ( 𝐼 Mat 𝑅 ) ) = ( Unit ‘ ( ∅ Mat 𝑅 ) ) ) → ( 𝑀 ∈ ( Unit ‘ ( 𝐼 Mat 𝑅 ) ) ↔ ∅ ∈ ( Unit ‘ ( ∅ Mat 𝑅 ) ) ) )
43 41 42 sylan2 ⊢ ( ( 𝑀 = ∅ ∧ 𝐼 = ∅ ) → ( 𝑀 ∈ ( Unit ‘ ( 𝐼 Mat 𝑅 ) ) ↔ ∅ ∈ ( Unit ‘ ( ∅ Mat 𝑅 ) ) ) )
44 cureq ⊢ ( 𝑀 = ∅ → curry 𝑀 = curry ∅ )
45 df-cur ⊢ curry ∅ = ( 𝑥 ∈ dom dom ∅ ↦ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ ∅ 𝑧 } )
46 24 dmeqi ⊢ dom dom ∅ = dom ∅
47 46 24 eqtri ⊢ dom dom ∅ = ∅
48 mpteq1 ⊢ ( dom dom ∅ = ∅ → ( 𝑥 ∈ dom dom ∅ ↦ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ ∅ 𝑧 } ) = ( 𝑥 ∈ ∅ ↦ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ ∅ 𝑧 } ) )
49 47 48 ax-mp ⊢ ( 𝑥 ∈ dom dom ∅ ↦ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ ∅ 𝑧 } ) = ( 𝑥 ∈ ∅ ↦ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ ∅ 𝑧 } )
50 mpt0 ⊢ ( 𝑥 ∈ ∅ ↦ { ⟨ 𝑦 , 𝑧 ⟩ ∣ ⟨ 𝑥 , 𝑦 ⟩ ∅ 𝑧 } ) = ∅
51 45 49 50 3eqtri ⊢ curry ∅ = ∅
52 44 51 eqtrdi ⊢ ( 𝑀 = ∅ → curry 𝑀 = ∅ )
53 oveq2 ⊢ ( 𝐼 = ∅ → ( 𝑅 freeLMod 𝐼 ) = ( 𝑅 freeLMod ∅ ) )
54 52 53 breqan12d ⊢ ( ( 𝑀 = ∅ ∧ 𝐼 = ∅ ) → ( curry 𝑀 LIndF ( 𝑅 freeLMod 𝐼 ) ↔ ∅ LIndF ( 𝑅 freeLMod ∅ ) ) )
55 43 54 bibi12d ⊢ ( ( 𝑀 = ∅ ∧ 𝐼 = ∅ ) → ( ( 𝑀 ∈ ( Unit ‘ ( 𝐼 Mat 𝑅 ) ) ↔ curry 𝑀 LIndF ( 𝑅 freeLMod 𝐼 ) ) ↔ ( ∅ ∈ ( Unit ‘ ( ∅ Mat 𝑅 ) ) ↔ ∅ LIndF ( 𝑅 freeLMod ∅ ) ) ) )
56 55 biimparc ⊢ ( ( ( ∅ ∈ ( Unit ‘ ( ∅ Mat 𝑅 ) ) ↔ ∅ LIndF ( 𝑅 freeLMod ∅ ) ) ∧ ( 𝑀 = ∅ ∧ 𝐼 = ∅ ) ) → ( 𝑀 ∈ ( Unit ‘ ( 𝐼 Mat 𝑅 ) ) ↔ curry 𝑀 LIndF ( 𝑅 freeLMod 𝐼 ) ) )
57 40 56 sylan ⊢ ( ( 𝑅 ∈ Field ∧ ( 𝑀 = ∅ ∧ 𝐼 = ∅ ) ) → ( 𝑀 ∈ ( Unit ‘ ( 𝐼 Mat 𝑅 ) ) ↔ curry 𝑀 LIndF ( 𝑅 freeLMod 𝐼 ) ) )
58 57 anassrs ⊢ ( ( ( 𝑅 ∈ Field ∧ 𝑀 = ∅ ) ∧ 𝐼 = ∅ ) → ( 𝑀 ∈ ( Unit ‘ ( 𝐼 Mat 𝑅 ) ) ↔ curry 𝑀 LIndF ( 𝑅 freeLMod 𝐼 ) ) )
59 8 58 sylancom ⊢ ( ( ( 𝑅 ∈ Field ∧ 𝑀 ∈ ( Base ‘ ( 𝐼 Mat 𝑅 ) ) ) ∧ 𝐼 = ∅ ) → ( 𝑀 ∈ ( Unit ‘ ( 𝐼 Mat 𝑅 ) ) ↔ curry 𝑀 LIndF ( 𝑅 freeLMod 𝐼 ) ) )
60 9 simprbi ⊢ ( 𝑅 ∈ Field → 𝑅 ∈ CRing )
61 eqid ⊢ ( 𝐼 Mat 𝑅 ) = ( 𝐼 Mat 𝑅 )
62 eqid ⊢ ( 𝐼 maDet 𝑅 ) = ( 𝐼 maDet 𝑅 )
63 eqid ⊢ ( Base ‘ ( 𝐼 Mat 𝑅 ) ) = ( Base ‘ ( 𝐼 Mat 𝑅 ) )
64 eqid ⊢ ( Unit ‘ ( 𝐼 Mat 𝑅 ) ) = ( Unit ‘ ( 𝐼 Mat 𝑅 ) )
65 eqid ⊢ ( Unit ‘ 𝑅 ) = ( Unit ‘ 𝑅 )
66 61 62 63 64 65 matunit ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( Base ‘ ( 𝐼 Mat 𝑅 ) ) ) → ( 𝑀 ∈ ( Unit ‘ ( 𝐼 Mat 𝑅 ) ) ↔ ( ( 𝐼 maDet 𝑅 ) ‘ 𝑀 ) ∈ ( Unit ‘ 𝑅 ) ) )
67 60 66 sylan ⊢ ( ( 𝑅 ∈ Field ∧ 𝑀 ∈ ( Base ‘ ( 𝐼 Mat 𝑅 ) ) ) → ( 𝑀 ∈ ( Unit ‘ ( 𝐼 Mat 𝑅 ) ) ↔ ( ( 𝐼 maDet 𝑅 ) ‘ 𝑀 ) ∈ ( Unit ‘ 𝑅 ) ) )
68 67 adantr ⊢ ( ( ( 𝑅 ∈ Field ∧ 𝑀 ∈ ( Base ‘ ( 𝐼 Mat 𝑅 ) ) ) ∧ 𝐼 ≠ ∅ ) → ( 𝑀 ∈ ( Unit ‘ ( 𝐼 Mat 𝑅 ) ) ↔ ( ( 𝐼 maDet 𝑅 ) ‘ 𝑀 ) ∈ ( Unit ‘ 𝑅 ) ) )
69 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
70 eqid ⊢ ( 0g ‘ 𝑅 ) = ( 0g ‘ 𝑅 )
71 69 65 70 drngunit ⊢ ( 𝑅 ∈ DivRing → ( ( ( 𝐼 maDet 𝑅 ) ‘ 𝑀 ) ∈ ( Unit ‘ 𝑅 ) ↔ ( ( ( 𝐼 maDet 𝑅 ) ‘ 𝑀 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝐼 maDet 𝑅 ) ‘ 𝑀 ) ≠ ( 0g ‘ 𝑅 ) ) ) )
72 10 71 syl ⊢ ( 𝑅 ∈ Field → ( ( ( 𝐼 maDet 𝑅 ) ‘ 𝑀 ) ∈ ( Unit ‘ 𝑅 ) ↔ ( ( ( 𝐼 maDet 𝑅 ) ‘ 𝑀 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝐼 maDet 𝑅 ) ‘ 𝑀 ) ≠ ( 0g ‘ 𝑅 ) ) ) )
73 72 adantr ⊢ ( ( 𝑅 ∈ Field ∧ 𝑀 ∈ ( Base ‘ ( 𝐼 Mat 𝑅 ) ) ) → ( ( ( 𝐼 maDet 𝑅 ) ‘ 𝑀 ) ∈ ( Unit ‘ 𝑅 ) ↔ ( ( ( 𝐼 maDet 𝑅 ) ‘ 𝑀 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝐼 maDet 𝑅 ) ‘ 𝑀 ) ≠ ( 0g ‘ 𝑅 ) ) ) )
74 62 61 63 69 mdetcl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ ( Base ‘ ( 𝐼 Mat 𝑅 ) ) ) → ( ( 𝐼 maDet 𝑅 ) ‘ 𝑀 ) ∈ ( Base ‘ 𝑅 ) )
75 60 74 sylan ⊢ ( ( 𝑅 ∈ Field ∧ 𝑀 ∈ ( Base ‘ ( 𝐼 Mat 𝑅 ) ) ) → ( ( 𝐼 maDet 𝑅 ) ‘ 𝑀 ) ∈ ( Base ‘ 𝑅 ) )
76 75 biantrurd ⊢ ( ( 𝑅 ∈ Field ∧ 𝑀 ∈ ( Base ‘ ( 𝐼 Mat 𝑅 ) ) ) → ( ( ( 𝐼 maDet 𝑅 ) ‘ 𝑀 ) ≠ ( 0g ‘ 𝑅 ) ↔ ( ( ( 𝐼 maDet 𝑅 ) ‘ 𝑀 ) ∈ ( Base ‘ 𝑅 ) ∧ ( ( 𝐼 maDet 𝑅 ) ‘ 𝑀 ) ≠ ( 0g ‘ 𝑅 ) ) ) )
77 73 76 bitr4d ⊢ ( ( 𝑅 ∈ Field ∧ 𝑀 ∈ ( Base ‘ ( 𝐼 Mat 𝑅 ) ) ) → ( ( ( 𝐼 maDet 𝑅 ) ‘ 𝑀 ) ∈ ( Unit ‘ 𝑅 ) ↔ ( ( 𝐼 maDet 𝑅 ) ‘ 𝑀 ) ≠ ( 0g ‘ 𝑅 ) ) )
78 77 adantr ⊢ ( ( ( 𝑅 ∈ Field ∧ 𝑀 ∈ ( Base ‘ ( 𝐼 Mat 𝑅 ) ) ) ∧ 𝐼 ≠ ∅ ) → ( ( ( 𝐼 maDet 𝑅 ) ‘ 𝑀 ) ∈ ( Unit ‘ 𝑅 ) ↔ ( ( 𝐼 maDet 𝑅 ) ‘ 𝑀 ) ≠ ( 0g ‘ 𝑅 ) ) )
79 61 63 matrcl ⊢ ( 𝑀 ∈ ( Base ‘ ( 𝐼 Mat 𝑅 ) ) → ( 𝐼 ∈ Fin ∧ 𝑅 ∈ V ) )
80 79 simpld ⊢ ( 𝑀 ∈ ( Base ‘ ( 𝐼 Mat 𝑅 ) ) → 𝐼 ∈ Fin )
81 80 pm4.71i ⊢ ( 𝑀 ∈ ( Base ‘ ( 𝐼 Mat 𝑅 ) ) ↔ ( 𝑀 ∈ ( Base ‘ ( 𝐼 Mat 𝑅 ) ) ∧ 𝐼 ∈ Fin ) )
82 xpfi ⊢ ( ( 𝐼 ∈ Fin ∧ 𝐼 ∈ Fin ) → ( 𝐼 × 𝐼 ) ∈ Fin )
83 82 anidms ⊢ ( 𝐼 ∈ Fin → ( 𝐼 × 𝐼 ) ∈ Fin )
84 eqid ⊢ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) = ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) )
85 84 69 frlmfibas ⊢ ( ( 𝑅 ∈ Field ∧ ( 𝐼 × 𝐼 ) ∈ Fin ) → ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 × 𝐼 ) ) = ( Base ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ) )
86 83 85 sylan2 ⊢ ( ( 𝑅 ∈ Field ∧ 𝐼 ∈ Fin ) → ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 × 𝐼 ) ) = ( Base ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ) )
87 61 84 matbas ⊢ ( ( 𝐼 ∈ Fin ∧ 𝑅 ∈ Field ) → ( Base ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ) = ( Base ‘ ( 𝐼 Mat 𝑅 ) ) )
88 87 ancoms ⊢ ( ( 𝑅 ∈ Field ∧ 𝐼 ∈ Fin ) → ( Base ‘ ( 𝑅 freeLMod ( 𝐼 × 𝐼 ) ) ) = ( Base ‘ ( 𝐼 Mat 𝑅 ) ) )
89 86 88 eqtrd ⊢ ( ( 𝑅 ∈ Field ∧ 𝐼 ∈ Fin ) → ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 × 𝐼 ) ) = ( Base ‘ ( 𝐼 Mat 𝑅 ) ) )
90 89 eleq2d ⊢ ( ( 𝑅 ∈ Field ∧ 𝐼 ∈ Fin ) → ( 𝑀 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 × 𝐼 ) ) ↔ 𝑀 ∈ ( Base ‘ ( 𝐼 Mat 𝑅 ) ) ) )
91 fvex ⊢ ( Base ‘ 𝑅 ) ∈ V
92 elmapg ⊢ ( ( ( Base ‘ 𝑅 ) ∈ V ∧ ( 𝐼 × 𝐼 ) ∈ Fin ) → ( 𝑀 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 × 𝐼 ) ) ↔ 𝑀 : ( 𝐼 × 𝐼 ) ⟶ ( Base ‘ 𝑅 ) ) )
93 91 83 92 sylancr ⊢ ( 𝐼 ∈ Fin → ( 𝑀 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 × 𝐼 ) ) ↔ 𝑀 : ( 𝐼 × 𝐼 ) ⟶ ( Base ‘ 𝑅 ) ) )
94 93 adantl ⊢ ( ( 𝑅 ∈ Field ∧ 𝐼 ∈ Fin ) → ( 𝑀 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝐼 × 𝐼 ) ) ↔ 𝑀 : ( 𝐼 × 𝐼 ) ⟶ ( Base ‘ 𝑅 ) ) )
95 90 94 bitr3d ⊢ ( ( 𝑅 ∈ Field ∧ 𝐼 ∈ Fin ) → ( 𝑀 ∈ ( Base ‘ ( 𝐼 Mat 𝑅 ) ) ↔ 𝑀 : ( 𝐼 × 𝐼 ) ⟶ ( Base ‘ 𝑅 ) ) )
96 95 ex ⊢ ( 𝑅 ∈ Field → ( 𝐼 ∈ Fin → ( 𝑀 ∈ ( Base ‘ ( 𝐼 Mat 𝑅 ) ) ↔ 𝑀 : ( 𝐼 × 𝐼 ) ⟶ ( Base ‘ 𝑅 ) ) ) )
97 96 pm5.32rd ⊢ ( 𝑅 ∈ Field → ( ( 𝑀 ∈ ( Base ‘ ( 𝐼 Mat 𝑅 ) ) ∧ 𝐼 ∈ Fin ) ↔ ( 𝑀 : ( 𝐼 × 𝐼 ) ⟶ ( Base ‘ 𝑅 ) ∧ 𝐼 ∈ Fin ) ) )
98 81 97 syl5bb ⊢ ( 𝑅 ∈ Field → ( 𝑀 ∈ ( Base ‘ ( 𝐼 Mat 𝑅 ) ) ↔ ( 𝑀 : ( 𝐼 × 𝐼 ) ⟶ ( Base ‘ 𝑅 ) ∧ 𝐼 ∈ Fin ) ) )
99 98 biimpd ⊢ ( 𝑅 ∈ Field → ( 𝑀 ∈ ( Base ‘ ( 𝐼 Mat 𝑅 ) ) → ( 𝑀 : ( 𝐼 × 𝐼 ) ⟶ ( Base ‘ 𝑅 ) ∧ 𝐼 ∈ Fin ) ) )
100 99 imdistani ⊢ ( ( 𝑅 ∈ Field ∧ 𝑀 ∈ ( Base ‘ ( 𝐼 Mat 𝑅 ) ) ) → ( 𝑅 ∈ Field ∧ ( 𝑀 : ( 𝐼 × 𝐼 ) ⟶ ( Base ‘ 𝑅 ) ∧ 𝐼 ∈ Fin ) ) )
101 anass ⊢ ( ( ( 𝑅 ∈ Field ∧ 𝑀 : ( 𝐼 × 𝐼 ) ⟶ ( Base ‘ 𝑅 ) ) ∧ 𝐼 ∈ Fin ) ↔ ( 𝑅 ∈ Field ∧ ( 𝑀 : ( 𝐼 × 𝐼 ) ⟶ ( Base ‘ 𝑅 ) ∧ 𝐼 ∈ Fin ) ) )
102 100 101 sylibr ⊢ ( ( 𝑅 ∈ Field ∧ 𝑀 ∈ ( Base ‘ ( 𝐼 Mat 𝑅 ) ) ) → ( ( 𝑅 ∈ Field ∧ 𝑀 : ( 𝐼 × 𝐼 ) ⟶ ( Base ‘ 𝑅 ) ) ∧ 𝐼 ∈ Fin ) )
103 eldifsn ⊢ ( 𝐼 ∈ ( Fin ∖ { ∅ } ) ↔ ( 𝐼 ∈ Fin ∧ 𝐼 ≠ ∅ ) )
104 matunitlindflem1 ⊢ ( ( ( 𝑅 ∈ Field ∧ 𝑀 : ( 𝐼 × 𝐼 ) ⟶ ( Base ‘ 𝑅 ) ) ∧ 𝐼 ∈ ( Fin ∖ { ∅ } ) ) → ( ¬ curry 𝑀 LIndF ( 𝑅 freeLMod 𝐼 ) → ( ( 𝐼 maDet 𝑅 ) ‘ 𝑀 ) = ( 0g ‘ 𝑅 ) ) )
105 104 necon1ad ⊢ ( ( ( 𝑅 ∈ Field ∧ 𝑀 : ( 𝐼 × 𝐼 ) ⟶ ( Base ‘ 𝑅 ) ) ∧ 𝐼 ∈ ( Fin ∖ { ∅ } ) ) → ( ( ( 𝐼 maDet 𝑅 ) ‘ 𝑀 ) ≠ ( 0g ‘ 𝑅 ) → curry 𝑀 LIndF ( 𝑅 freeLMod 𝐼 ) ) )
106 103 105 sylan2br ⊢ ( ( ( 𝑅 ∈ Field ∧ 𝑀 : ( 𝐼 × 𝐼 ) ⟶ ( Base ‘ 𝑅 ) ) ∧ ( 𝐼 ∈ Fin ∧ 𝐼 ≠ ∅ ) ) → ( ( ( 𝐼 maDet 𝑅 ) ‘ 𝑀 ) ≠ ( 0g ‘ 𝑅 ) → curry 𝑀 LIndF ( 𝑅 freeLMod 𝐼 ) ) )
107 106 anassrs ⊢ ( ( ( ( 𝑅 ∈ Field ∧ 𝑀 : ( 𝐼 × 𝐼 ) ⟶ ( Base ‘ 𝑅 ) ) ∧ 𝐼 ∈ Fin ) ∧ 𝐼 ≠ ∅ ) → ( ( ( 𝐼 maDet 𝑅 ) ‘ 𝑀 ) ≠ ( 0g ‘ 𝑅 ) → curry 𝑀 LIndF ( 𝑅 freeLMod 𝐼 ) ) )
108 102 107 sylan ⊢ ( ( ( 𝑅 ∈ Field ∧ 𝑀 ∈ ( Base ‘ ( 𝐼 Mat 𝑅 ) ) ) ∧ 𝐼 ≠ ∅ ) → ( ( ( 𝐼 maDet 𝑅 ) ‘ 𝑀 ) ≠ ( 0g ‘ 𝑅 ) → curry 𝑀 LIndF ( 𝑅 freeLMod 𝐼 ) ) )
109 78 108 sylbid ⊢ ( ( ( 𝑅 ∈ Field ∧ 𝑀 ∈ ( Base ‘ ( 𝐼 Mat 𝑅 ) ) ) ∧ 𝐼 ≠ ∅ ) → ( ( ( 𝐼 maDet 𝑅 ) ‘ 𝑀 ) ∈ ( Unit ‘ 𝑅 ) → curry 𝑀 LIndF ( 𝑅 freeLMod 𝐼 ) ) )
110 matunitlindflem2 ⊢ ( ( ( ( 𝑅 ∈ Field ∧ 𝑀 ∈ ( Base ‘ ( 𝐼 Mat 𝑅 ) ) ) ∧ 𝐼 ≠ ∅ ) ∧ curry 𝑀 LIndF ( 𝑅 freeLMod 𝐼 ) ) → ( ( 𝐼 maDet 𝑅 ) ‘ 𝑀 ) ∈ ( Unit ‘ 𝑅 ) )
111 110 ex ⊢ ( ( ( 𝑅 ∈ Field ∧ 𝑀 ∈ ( Base ‘ ( 𝐼 Mat 𝑅 ) ) ) ∧ 𝐼 ≠ ∅ ) → ( curry 𝑀 LIndF ( 𝑅 freeLMod 𝐼 ) → ( ( 𝐼 maDet 𝑅 ) ‘ 𝑀 ) ∈ ( Unit ‘ 𝑅 ) ) )
112 109 111 impbid ⊢ ( ( ( 𝑅 ∈ Field ∧ 𝑀 ∈ ( Base ‘ ( 𝐼 Mat 𝑅 ) ) ) ∧ 𝐼 ≠ ∅ ) → ( ( ( 𝐼 maDet 𝑅 ) ‘ 𝑀 ) ∈ ( Unit ‘ 𝑅 ) ↔ curry 𝑀 LIndF ( 𝑅 freeLMod 𝐼 ) ) )
113 68 112 bitrd ⊢ ( ( ( 𝑅 ∈ Field ∧ 𝑀 ∈ ( Base ‘ ( 𝐼 Mat 𝑅 ) ) ) ∧ 𝐼 ≠ ∅ ) → ( 𝑀 ∈ ( Unit ‘ ( 𝐼 Mat 𝑅 ) ) ↔ curry 𝑀 LIndF ( 𝑅 freeLMod 𝐼 ) ) )
114 59 113 pm2.61dane ⊢ ( ( 𝑅 ∈ Field ∧ 𝑀 ∈ ( Base ‘ ( 𝐼 Mat 𝑅 ) ) ) → ( 𝑀 ∈ ( Unit ‘ ( 𝐼 Mat 𝑅 ) ) ↔ curry 𝑀 LIndF ( 𝑅 freeLMod 𝐼 ) ) )