Metamath Proof Explorer

Theorem slesolinvbi

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, 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 )
slesolinv.i 
|- I = ( invr ` A )
Assertion slesolinvbi 
|- ( ( ( 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 simpl1 
 |-  ( ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) /\ ( X .x. Z ) = Y ) -> ( N =/= (/) /\ R e. CRing ) )
8 simpl2 
 |-  ( ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) /\ ( X .x. Z ) = Y ) -> ( X e. B /\ Y e. V ) )
9 simp3 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( D ` X ) e. ( Unit ` R ) )
10 9 anim1i 
 |-  ( ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) /\ ( X .x. Z ) = Y ) -> ( ( D ` X ) e. ( Unit ` R ) /\ ( X .x. Z ) = Y ) )
11 1 2 3 4 5 6 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 ) )
12 7 8 10 11 syl3anc 
 |-  ( ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) /\ ( X .x. Z ) = Y ) -> Z = ( ( I ` X ) .x. Y ) )
13 oveq2 
 |-  ( Z = ( ( I ` X ) .x. Y ) -> ( X .x. Z ) = ( X .x. ( ( I ` X ) .x. Y ) ) )
14 simpr 
 |-  ( ( N =/= (/) /\ R e. CRing ) -> R e. CRing )
15 1 2 matrcl 
 |-  ( X e. B -> ( N e. Fin /\ R e. _V ) )
16 15 simpld 
 |-  ( X e. B -> N e. Fin )
17 16 adantr 
 |-  ( ( X e. B /\ Y e. V ) -> N e. Fin )
18 14 17 anim12ci 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) ) -> ( N e. Fin /\ R e. CRing ) )
19 18 3adant3 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( N e. Fin /\ R e. CRing ) )
20 eqid 
 |-  ( R maMul <. N , N , N >. ) = ( R maMul <. N , N , N >. )
21 1 20 matmulr 
 |-  ( ( N e. Fin /\ R e. CRing ) -> ( R maMul <. N , N , N >. ) = ( .r ` A ) )
22 19 21 syl 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( R maMul <. N , N , N >. ) = ( .r ` A ) )
23 22 oveqd 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( X ( R maMul <. N , N , N >. ) ( I ` X ) ) = ( X ( .r ` A ) ( I ` X ) ) )
24 crngring 
 |-  ( R e. CRing -> R e. Ring )
25 24 adantl 
 |-  ( ( N =/= (/) /\ R e. CRing ) -> R e. Ring )
26 25 17 anim12ci 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) ) -> ( N e. Fin /\ R e. Ring ) )
27 26 3adant3 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( N e. Fin /\ R e. Ring ) )
28 1 matring 
 |-  ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
29 27 28 syl 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> A e. Ring )
30 eqid 
 |-  ( Unit ` A ) = ( Unit ` A )
31 eqid 
 |-  ( Unit ` R ) = ( Unit ` R )
32 1 5 2 30 31 matunit 
 |-  ( ( R e. CRing /\ X e. B ) -> ( X e. ( Unit ` A ) <-> ( D ` X ) e. ( Unit ` R ) ) )
33 32 ad2ant2lr 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) ) -> ( X e. ( Unit ` A ) <-> ( D ` X ) e. ( Unit ` R ) ) )
34 33 biimp3ar 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> X e. ( Unit ` A ) )
35 eqid 
 |-  ( .r ` A ) = ( .r ` A )
36 eqid 
 |-  ( 1r ` A ) = ( 1r ` A )
37 30 6 35 36 unitrinv 
 |-  ( ( A e. Ring /\ X e. ( Unit ` A ) ) -> ( X ( .r ` A ) ( I ` X ) ) = ( 1r ` A ) )
38 29 34 37 syl2anc 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( X ( .r ` A ) ( I ` X ) ) = ( 1r ` A ) )
39 23 38 eqtrd 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( X ( R maMul <. N , N , N >. ) ( I ` X ) ) = ( 1r ` A ) )
40 39 oveq1d 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( ( X ( R maMul <. N , N , N >. ) ( I ` X ) ) .x. Y ) = ( ( 1r ` A ) .x. Y ) )
41 eqid 
 |-  ( Base ` R ) = ( Base ` R )
42 25 3ad2ant1 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> R e. Ring )
43 17 3ad2ant2 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> N e. Fin )
44 3 eleq2i 
 |-  ( Y e. V <-> Y e. ( ( Base ` R ) ^m N ) )
45 44 biimpi 
 |-  ( Y e. V -> Y e. ( ( Base ` R ) ^m N ) )
46 45 adantl 
 |-  ( ( X e. B /\ Y e. V ) -> Y e. ( ( Base ` R ) ^m N ) )
47 46 3ad2ant2 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> Y e. ( ( Base ` R ) ^m N ) )
48 2 eleq2i 
 |-  ( X e. B <-> X e. ( Base ` A ) )
49 48 biimpi 
 |-  ( X e. B -> X e. ( Base ` A ) )
50 49 adantr 
 |-  ( ( X e. B /\ Y e. V ) -> X e. ( Base ` A ) )
51 50 3ad2ant2 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> X e. ( Base ` A ) )
52 eqid 
 |-  ( Base ` A ) = ( Base ` A )
53 30 6 52 ringinvcl 
 |-  ( ( A e. Ring /\ X e. ( Unit ` A ) ) -> ( I ` X ) e. ( Base ` A ) )
54 29 34 53 syl2anc 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( I ` X ) e. ( Base ` A ) )
55 1 41 4 42 43 47 20 51 54 mavmulass 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( ( X ( R maMul <. N , N , N >. ) ( I ` X ) ) .x. Y ) = ( X .x. ( ( I ` X ) .x. Y ) ) )
56 1 41 4 42 43 47 1mavmul 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( ( 1r ` A ) .x. Y ) = Y )
57 40 55 56 3eqtr3d 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( X .x. ( ( I ` X ) .x. Y ) ) = Y )
58 13 57 sylan9eqr 
 |-  ( ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) /\ Z = ( ( I ` X ) .x. Y ) ) -> ( X .x. Z ) = Y )
59 12 58 impbida 
 |-  ( ( ( N =/= (/) /\ R e. CRing ) /\ ( X e. B /\ Y e. V ) /\ ( D ` X ) e. ( Unit ` R ) ) -> ( ( X .x. Z ) = Y <-> Z = ( ( I ` X ) .x. Y ) ) )