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=NMatR
slesolex.b B=BaseA
slesolex.v V=BaseRN
slesolex.x ·˙=RmaVecMulNN
slesolex.d D=NmaDetR
slesolinv.i I=invrA
Assertion slesolinvbi NRCRingXBYVDXUnitRX·˙Z=YZ=IX·˙Y

Proof

Step Hyp Ref Expression
1 slesolex.a A=NMatR
2 slesolex.b B=BaseA
3 slesolex.v V=BaseRN
4 slesolex.x ·˙=RmaVecMulNN
5 slesolex.d D=NmaDetR
6 slesolinv.i I=invrA
7 simpl1 NRCRingXBYVDXUnitRX·˙Z=YNRCRing
8 simpl2 NRCRingXBYVDXUnitRX·˙Z=YXBYV
9 simp3 NRCRingXBYVDXUnitRDXUnitR
10 9 anim1i NRCRingXBYVDXUnitRX·˙Z=YDXUnitRX·˙Z=Y
11 1 2 3 4 5 6 slesolinv NRCRingXBYVDXUnitRX·˙Z=YZ=IX·˙Y
12 7 8 10 11 syl3anc NRCRingXBYVDXUnitRX·˙Z=YZ=IX·˙Y
13 oveq2 Z=IX·˙YX·˙Z=X·˙IX·˙Y
14 simpr NRCRingRCRing
15 1 2 matrcl XBNFinRV
16 15 simpld XBNFin
17 16 adantr XBYVNFin
18 14 17 anim12ci NRCRingXBYVNFinRCRing
19 18 3adant3 NRCRingXBYVDXUnitRNFinRCRing
20 eqid RmaMulNNN=RmaMulNNN
21 1 20 matmulr NFinRCRingRmaMulNNN=A
22 19 21 syl NRCRingXBYVDXUnitRRmaMulNNN=A
23 22 oveqd NRCRingXBYVDXUnitRXRmaMulNNNIX=XAIX
24 crngring RCRingRRing
25 24 adantl NRCRingRRing
26 25 17 anim12ci NRCRingXBYVNFinRRing
27 26 3adant3 NRCRingXBYVDXUnitRNFinRRing
28 1 matring NFinRRingARing
29 27 28 syl NRCRingXBYVDXUnitRARing
30 eqid UnitA=UnitA
31 eqid UnitR=UnitR
32 1 5 2 30 31 matunit RCRingXBXUnitADXUnitR
33 32 ad2ant2lr NRCRingXBYVXUnitADXUnitR
34 33 biimp3ar NRCRingXBYVDXUnitRXUnitA
35 eqid A=A
36 eqid 1A=1A
37 30 6 35 36 unitrinv ARingXUnitAXAIX=1A
38 29 34 37 syl2anc NRCRingXBYVDXUnitRXAIX=1A
39 23 38 eqtrd NRCRingXBYVDXUnitRXRmaMulNNNIX=1A
40 39 oveq1d NRCRingXBYVDXUnitRXRmaMulNNNIX·˙Y=1A·˙Y
41 eqid BaseR=BaseR
42 25 3ad2ant1 NRCRingXBYVDXUnitRRRing
43 17 3ad2ant2 NRCRingXBYVDXUnitRNFin
44 3 eleq2i YVYBaseRN
45 44 biimpi YVYBaseRN
46 45 adantl XBYVYBaseRN
47 46 3ad2ant2 NRCRingXBYVDXUnitRYBaseRN
48 2 eleq2i XBXBaseA
49 48 biimpi XBXBaseA
50 49 adantr XBYVXBaseA
51 50 3ad2ant2 NRCRingXBYVDXUnitRXBaseA
52 eqid BaseA=BaseA
53 30 6 52 ringinvcl ARingXUnitAIXBaseA
54 29 34 53 syl2anc NRCRingXBYVDXUnitRIXBaseA
55 1 41 4 42 43 47 20 51 54 mavmulass NRCRingXBYVDXUnitRXRmaMulNNNIX·˙Y=X·˙IX·˙Y
56 1 41 4 42 43 47 1mavmul NRCRingXBYVDXUnitR1A·˙Y=Y
57 40 55 56 3eqtr3d NRCRingXBYVDXUnitRX·˙IX·˙Y=Y
58 13 57 sylan9eqr NRCRingXBYVDXUnitRZ=IX·˙YX·˙Z=Y
59 12 58 impbida NRCRingXBYVDXUnitRX·˙Z=YZ=IX·˙Y