Metamath Proof Explorer

Theorem slesolinv

Description: The solution of a system of linear equations represented by a matrix with a unit as determinant is the multiplication of the inverse of the matrix with the right-hand side vector. (Contributed by AV, 10-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 )
slesolinv.i 
|- I = ( invr ` A )
Assertion slesolinv 
|- ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. ( Unit ` R ) /\ ( X .x. Z ) = Y ) ) -> Z = ( ( I ` X ) .x. 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 slesolinv.i 
 |-  I = ( invr ` A )
7 eqid 
 |-  ( Base ` R ) = ( Base ` 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 ) /\ ( X .x. Z ) = Y ) ) -> 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 ) /\ ( X .x. Z ) = Y ) ) -> N e. Fin )
15 8 anim2i 
 |-  ( ( N =/= (/) /\ R e. CRing ) -> ( N =/= (/) /\ R e. Ring ) )
16 15 anim1i 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) ) -> ( ( N =/= (/) /\ R e. Ring ) /\ ( X e. B /\ Y e. V ) ) )
17 16 3adant3 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. ( Unit ` R ) /\ ( X .x. Z ) = Y ) ) -> ( ( N =/= (/) /\ R e. Ring ) /\ ( X e. B /\ Y e. V ) ) )
18 simpr 
 |-  ( ( ( D ` X ) e. ( Unit ` R ) /\ ( X .x. Z ) = Y ) -> ( X .x. Z ) = Y )
19 18 3ad2ant3 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. ( Unit ` R ) /\ ( X .x. Z ) = Y ) ) -> ( X .x. Z ) = Y )
20 1 2 3 4 slesolvec 
 |-  ( ( ( N =/= (/) /\ R e. Ring ) /\ ( X e. B /\ Y e. V ) ) -> ( ( X .x. Z ) = Y -> Z e. V ) )
21 17 19 20 sylc 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. ( Unit ` R ) /\ ( X .x. Z ) = Y ) ) -> Z e. V )
22 21 3 eleqtrdi 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. ( Unit ` R ) /\ ( X .x. Z ) = Y ) ) -> Z e. ( ( Base ` R ) ^m N ) )
23 eqid 
 |-  ( R maMul <. N , N , N >. ) = ( R maMul <. N , N , N >. )
24 9 13 anim12ci 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) ) -> ( N e. Fin /\ R e. Ring ) )
25 24 3adant3 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. ( Unit ` R ) /\ ( X .x. Z ) = Y ) ) -> ( N e. Fin /\ R e. Ring ) )
26 1 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
27 25 26 syl 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. ( Unit ` R ) /\ ( X .x. Z ) = Y ) ) -> A e. Ring )
28 eqid 
 |-  ( Unit ` A ) = ( Unit ` A )
29 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
30 1 5 2 28 29 matunit 
 |-  ( ( R e. CRing /\ X e. B ) -> ( X e. ( Unit ` A ) <-> ( D ` X ) e. ( Unit ` R ) ) )
31 30 bicomd 
 |-  ( ( R e. CRing /\ X e. B ) -> ( ( D ` X ) e. ( Unit ` R ) <-> X e. ( Unit ` A ) ) )
32 31 ad2ant2lr 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) ) -> ( ( D ` X ) e. ( Unit ` R ) <-> X e. ( Unit ` A ) ) )
33 32 biimpd 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) ) -> ( ( D ` X ) e. ( Unit ` R ) -> X e. ( Unit ` A ) ) )
34 33 adantrd 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) ) -> ( ( ( D ` X ) e. ( Unit ` R ) /\ ( X .x. Z ) = Y ) -> X e. ( Unit ` A ) ) )
35 34 3impia 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. ( Unit ` R ) /\ ( X .x. Z ) = Y ) ) -> X e. ( Unit ` A ) )
36 eqid 
 |-  ( Base ` A ) = ( Base ` A )
37 28 6 36 ringinvcl 
 |-  ( ( A e. Ring /\ X e. ( Unit ` A ) ) -> ( I ` X ) e. ( Base ` A ) )
38 27 35 37 syl2anc 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. ( Unit ` R ) /\ ( X .x. Z ) = Y ) ) -> ( I ` X ) e. ( Base ` A ) )
39 2 eleq2i 
 |-  ( X e. B <-> X e. ( Base ` A ) )
40 39 biimpi 
 |-  ( X e. B -> X e. ( Base ` A ) )
41 40 adantr 
 |-  ( ( X e. B /\ Y e. V ) -> X e. ( Base ` A ) )
42 41 3ad2ant2 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. ( Unit ` R ) /\ ( X .x. Z ) = Y ) ) -> X e. ( Base ` A ) )
43 1 7 4 10 14 22 23 38 42 mavmulass 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. ( Unit ` R ) /\ ( X .x. Z ) = Y ) ) -> ( ( ( I ` X ) ( R maMul <. N , N , N >. ) X ) .x. Z ) = ( ( I ` X ) .x. ( X .x. Z ) ) )
44 simpr 
 |-  ( ( N =/= (/) /\ R e. CRing ) -> R e. CRing )
45 44 13 anim12ci 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) ) -> ( N e. Fin /\ R e. CRing ) )
46 45 3adant3 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. ( Unit ` R ) /\ ( X .x. Z ) = Y ) ) -> ( N e. Fin /\ R e. CRing ) )
47 1 23 matmulr 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( R maMul <. N , N , N >. ) = ( .r ` A ) )
48 46 47 syl 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. ( Unit ` R ) /\ ( X .x. Z ) = Y ) ) -> ( R maMul <. N , N , N >. ) = ( .r ` A ) )
49 48 oveqd 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. ( Unit ` R ) /\ ( X .x. Z ) = Y ) ) -> ( ( I ` X ) ( R maMul <. N , N , N >. ) X ) = ( ( I ` X ) ( .r ` A ) X ) )
50 eqid 
 |-  ( .r ` A ) = ( .r ` A )
51 eqid 
 |-  ( 1r ` A ) = ( 1r ` A )
52 28 6 50 51 unitlinv 
 |-  ( ( A e. Ring /\ X e. ( Unit ` A ) ) -> ( ( I ` X ) ( .r ` A ) X ) = ( 1r ` A ) )
53 27 35 52 syl2anc 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. ( Unit ` R ) /\ ( X .x. Z ) = Y ) ) -> ( ( I ` X ) ( .r ` A ) X ) = ( 1r ` A ) )
54 49 53 eqtrd 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. ( Unit ` R ) /\ ( X .x. Z ) = Y ) ) -> ( ( I ` X ) ( R maMul <. N , N , N >. ) X ) = ( 1r ` A ) )
55 54 oveq1d 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. ( Unit ` R ) /\ ( X .x. Z ) = Y ) ) -> ( ( ( I ` X ) ( R maMul <. N , N , N >. ) X ) .x. Z ) = ( ( 1r ` A ) .x. Z ) )
56 1 7 4 10 14 22 1mavmul 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. ( Unit ` R ) /\ ( X .x. Z ) = Y ) ) -> ( ( 1r ` A ) .x. Z ) = Z )
57 55 56 eqtrd 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. ( Unit ` R ) /\ ( X .x. Z ) = Y ) ) -> ( ( ( I ` X ) ( R maMul <. N , N , N >. ) X ) .x. Z ) = Z )
58 oveq2 
 |-  ( ( X .x. Z ) = Y -> ( ( I ` X ) .x. ( X .x. Z ) ) = ( ( I ` X ) .x. Y ) )
59 58 adantl 
 |-  ( ( ( D ` X ) e. ( Unit ` R ) /\ ( X .x. Z ) = Y ) -> ( ( I ` X ) .x. ( X .x. Z ) ) = ( ( I ` X ) .x. Y ) )
60 59 3ad2ant3 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. ( Unit ` R ) /\ ( X .x. Z ) = Y ) ) -> ( ( I ` X ) .x. ( X .x. Z ) ) = ( ( I ` X ) .x. Y ) )
61 43 57 60 3eqtr3d 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( ( D ` X ) e. ( Unit ` R ) /\ ( X .x. Z ) = Y ) ) -> Z = ( ( I ` X ) .x. Y ) )