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 )