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 
|- ( ( R e. Field /\ M e. ( Base ` ( I Mat R ) ) ) -> ( M e. ( Unit ` ( I Mat R ) ) <-> curry M LIndF ( R freeLMod I ) ) )

Proof

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