Metamath Proof Explorer


Theorem cramerimplem3

Description: Lemma 3 for cramerimp : The determinant of the matrix of a system of linear equations multiplied with the determinant of the identity matrix with the ith column replaced by the solution vector of the system of linear equations equals the determinant of the matrix of the system of linear equations with the ith column replaced by the right-hand side vector of the system of linear equations. (Contributed by AV, 19-Feb-2019) (Revised by AV, 1-Mar-2019)

Ref Expression
Hypotheses cramerimp.a A=NMatR
cramerimp.b B=BaseA
cramerimp.v V=BaseRN
cramerimp.e E=1ANmatRepVRZI
cramerimp.h H=XNmatRepVRYI
cramerimp.x ·˙=RmaVecMulNN
cramerimp.d D=NmaDetR
cramerimp.t ˙=R
Assertion cramerimplem3 RCRingINXBYVX·˙Z=YDX˙DE=DH

Proof

Step Hyp Ref Expression
1 cramerimp.a A=NMatR
2 cramerimp.b B=BaseA
3 cramerimp.v V=BaseRN
4 cramerimp.e E=1ANmatRepVRZI
5 cramerimp.h H=XNmatRepVRYI
6 cramerimp.x ·˙=RmaVecMulNN
7 cramerimp.d D=NmaDetR
8 cramerimp.t ˙=R
9 simpl RCRingINRCRing
10 1 2 matrcl XBNFinRV
11 10 simpld XBNFin
12 11 adantr XBYVNFin
13 9 12 anim12ci RCRingINXBYVNFinRCRing
14 13 3adant3 RCRingINXBYVX·˙Z=YNFinRCRing
15 eqid RmaMulNNN=RmaMulNNN
16 1 15 matmulr NFinRCRingRmaMulNNN=A
17 14 16 syl RCRingINXBYVX·˙Z=YRmaMulNNN=A
18 17 oveqd RCRingINXBYVX·˙Z=YXRmaMulNNNE=XAE
19 18 fveq2d RCRingINXBYVX·˙Z=YDXRmaMulNNNE=DXAE
20 1 2 3 4 5 6 15 cramerimplem2 RCRingINXBYVX·˙Z=YXRmaMulNNNE=H
21 20 fveq2d RCRingINXBYVX·˙Z=YDXRmaMulNNNE=DH
22 simp1l RCRingINXBYVX·˙Z=YRCRing
23 simp2l RCRingINXBYVX·˙Z=YXB
24 crngring RCRingRRing
25 24 adantr RCRingINRRing
26 25 12 anim12i RCRingINXBYVRRingNFin
27 26 3adant3 RCRingINXBYVX·˙Z=YRRingNFin
28 ne0i INN
29 24 28 anim12ci RCRingINNRRing
30 1 2 3 6 slesolvec NRRingXBYVX·˙Z=YZV
31 29 30 sylan RCRingINXBYVX·˙Z=YZV
32 31 3impia RCRingINXBYVX·˙Z=YZV
33 simp1r RCRingINXBYVX·˙Z=YIN
34 eqid 1A=1A
35 1 2 3 34 ma1repvcl RRingNFinZVIN1ANmatRepVRZIB
36 27 32 33 35 syl12anc RCRingINXBYVX·˙Z=Y1ANmatRepVRZIB
37 4 36 eqeltrid RCRingINXBYVX·˙Z=YEB
38 eqid A=A
39 1 2 7 8 38 mdetmul RCRingXBEBDXAE=DX˙DE
40 22 23 37 39 syl3anc RCRingINXBYVX·˙Z=YDXAE=DX˙DE
41 19 21 40 3eqtr3rd RCRingINXBYVX·˙Z=YDX˙DE=DH