Metamath Proof Explorer

Theorem slesolex

Description: Every system of linear equations represented by a matrix with a unit as determinant has a solution. (Contributed by AV, 11-Feb-2019) (Revised by AV, 28-Feb-2019)

Ref Expression
Hypotheses slesolex.a 
|- A = ( N Mat R )
slesolex.b 
|- B = ( Base ` A )
slesolex.v 
|- V = ( ( Base ` R ) ^m N )
slesolex.x 
|- .x. = ( R maVecMul <. N , N >. )
slesolex.d 
|- D = ( N maDet R )
Assertion slesolex 
|- ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> E. z e. V ( X .x. z ) = Y )

Proof

Step Hyp Ref Expression
1 slesolex.a 
 |-  A = ( N Mat R )
2 slesolex.b 
 |-  B = ( Base ` A )
3 slesolex.v 
 |-  V = ( ( Base ` R ) ^m N )
4 slesolex.x 
 |-  .x. = ( R maVecMul <. N , N >. )
5 slesolex.d 
 |-  D = ( N maDet R )
6 eqid 
 |-  ( Base ` R ) = ( Base ` R )
7 eqid 
 |-  ( .r ` R ) = ( .r ` R )
8 crngring 
 |-  ( R e. CRing -> R e. Ring )
9 8 adantl 
 |-  ( ( N =/= (/) /\ R e. CRing ) -> R e. Ring )
10 9 3ad2ant1 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> R e. Ring )
11 1 2 matrcl 
 |-  ( X e. B -> ( N e. Fin /\ R e. _V ) )
12 11 simpld 
 |-  ( X e. B -> N e. Fin )
13 12 adantr 
 |-  ( ( X e. B /\ Y e. V ) -> N e. Fin )
14 13 3ad2ant2 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> N e. Fin )
15 9 13 anim12ci 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) ) -> ( N e. Fin /\ R e. Ring ) )
16 15 3adant3 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( N e. Fin /\ R e. Ring ) )
17 1 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
18 16 17 syl 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> A e. Ring )
19 eqid 
 |-  ( Unit ` A ) = ( Unit ` A )
20 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
21 1 5 2 19 20 matunit 
 |-  ( ( R e. CRing /\ X e. B ) -> ( X e. ( Unit ` A ) <-> ( D ` X ) e. ( Unit ` R ) ) )
22 21 bicomd 
 |-  ( ( R e. CRing /\ X e. B ) -> ( ( D ` X ) e. ( Unit ` R ) <-> X e. ( Unit ` A ) ) )
23 22 ad2ant2lr 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) ) -> ( ( D ` X ) e. ( Unit ` R ) <-> X e. ( Unit ` A ) ) )
24 23 biimp3a 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> X e. ( Unit ` A ) )
25 eqid 
 |-  ( invr ` A ) = ( invr ` A )
26 eqid 
 |-  ( Base ` A ) = ( Base ` A )
27 19 25 26 ringinvcl 
 |-  ( ( A e. Ring /\ X e. ( Unit ` A ) ) -> ( ( invr ` A ) ` X ) e. ( Base ` A ) )
28 18 24 27 syl2anc 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( ( invr ` A ) ` X ) e. ( Base ` A ) )
29 3 eleq2i 
 |-  ( Y e. V <-> Y e. ( ( Base ` R ) ^m N ) )
30 29 biimpi 
 |-  ( Y e. V -> Y e. ( ( Base ` R ) ^m N ) )
31 30 adantl 
 |-  ( ( X e. B /\ Y e. V ) -> Y e. ( ( Base ` R ) ^m N ) )
32 31 3ad2ant2 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> Y e. ( ( Base ` R ) ^m N ) )
33 1 4 6 7 10 14 28 32 mavmulcl 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( ( ( invr ` A ) ` X ) .x. Y ) e. ( ( Base ` R ) ^m N ) )
34 33 3 eleqtrrdi 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( ( ( invr ` A ) ` X ) .x. Y ) e. V )
35 1 2 3 4 5 25 slesolinvbi 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( ( X .x. z ) = Y <-> z = ( ( ( invr ` A ) ` X ) .x. Y ) ) )
36 35 adantr 
 |-  ( ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) /\ ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) ) -> ( ( X .x. z ) = Y <-> z = ( ( ( invr ` A ) ` X ) .x. Y ) ) )
37 36 biimprd 
 |-  ( ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) /\ ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) ) -> ( z = ( ( ( invr ` A ) ` X ) .x. Y ) -> ( X .x. z ) = Y ) )
38 37 impancom 
 |-  ( ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) /\ z = ( ( ( invr ` A ) ` X ) .x. Y ) ) -> ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( X .x. z ) = Y ) )
39 34 38 rspcimedv 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> E. z e. V ( X .x. z ) = Y ) )
40 39 pm2.43i 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> E. z e. V ( X .x. z ) = Y )