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 syl6bi
 |-  ( ( 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 0fin
 |-  (/) 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 syl5bb
 |-  ( 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 ) ) )