Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  slesolinv Structured version   Visualization version   Unicode version

Theorem slesolinv 19698
 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.)
Hypotheses
Ref Expression
slesolex.a Mat
slesolex.b
slesolex.v
slesolex.x maVecMul
slesolinv.i
Assertion
Ref Expression
slesolinv Unit

Proof of Theorem slesolinv
StepHypRef Expression
1 slesolex.a . . 3 Mat
2 eqid 2450 . . 3
3 slesolex.x . . 3 maVecMul
4 crngring 17784 . . . . 5
54adantl 468 . . . 4
653ad2ant1 1028 . . 3 Unit
7 slesolex.b . . . . . . 7
81, 7matrcl 19430 . . . . . 6
98simpld 461 . . . . 5
109adantr 467 . . . 4
11103ad2ant2 1029 . . 3 Unit
124anim2i 572 . . . . . . 7
1312anim1i 571 . . . . . 6
14133adant3 1027 . . . . 5 Unit
15 simpr 463 . . . . . 6 Unit
16153ad2ant3 1030 . . . . 5 Unit
17 slesolex.v . . . . . 6
181, 7, 17, 3slesolvec 19697 . . . . 5
1914, 16, 18sylc 62 . . . 4 Unit
2019, 17syl6eleq 2538 . . 3 Unit
21 eqid 2450 . . 3 maMul maMul
225, 10anim12ci 570 . . . . . 6
23223adant3 1027 . . . . 5 Unit
241matring 19461 . . . . 5
2523, 24syl 17 . . . 4 Unit
26 slesolex.d . . . . . . . . . 10 maDet
27 eqid 2450 . . . . . . . . . 10 Unit Unit
28 eqid 2450 . . . . . . . . . 10 Unit Unit
291, 26, 7, 27, 28matunit 19696 . . . . . . . . 9 Unit Unit
3029bicomd 205 . . . . . . . 8 Unit Unit
3130ad2ant2lr 753 . . . . . . 7 Unit Unit
3231biimpd 211 . . . . . 6 Unit Unit
3332adantrd 470 . . . . 5 Unit Unit
34333impia 1204 . . . 4 Unit Unit
35 slesolinv.i . . . . 5
36 eqid 2450 . . . . 5
3727, 35, 36ringinvcl 17897 . . . 4 Unit
3825, 34, 37syl2anc 666 . . 3 Unit
397eleq2i 2520 . . . . . 6
4039biimpi 198 . . . . 5
4140adantr 467 . . . 4
42413ad2ant2 1029 . . 3 Unit
431, 2, 3, 6, 11, 20, 21, 38, 42mavmulass 19567 . 2 Unit maMul
44 simpr 463 . . . . . . . . 9
4544, 10anim12ci 570 . . . . . . . 8
46453adant3 1027 . . . . . . 7 Unit
471, 21matmulr 19456 . . . . . . 7 maMul
4846, 47syl 17 . . . . . 6 Unit maMul
4948oveqd 6305 . . . . 5 Unit maMul
50 eqid 2450 . . . . . . 7
51 eqid 2450 . . . . . . 7
5227, 35, 50, 51unitlinv 17898 . . . . . 6 Unit
5325, 34, 52syl2anc 666 . . . . 5 Unit
5449, 53eqtrd 2484 . . . 4 Unit maMul
5554oveq1d 6303 . . 3 Unit maMul
561, 2, 3, 6, 11, 201mavmul 19566 . . 3 Unit
5755, 56eqtrd 2484 . 2 Unit maMul
58 oveq2 6296 . . . 4
5958adantl 468 . . 3 Unit