Metamath Proof Explorer


Theorem cramerlem2

Description: Lemma 2 for cramer . (Contributed by AV, 21-Feb-2019) (Revised by AV, 1-Mar-2019)

Ref Expression
Hypotheses cramer.a A=NMatR
cramer.b B=BaseA
cramer.v V=BaseRN
cramer.d D=NmaDetR
cramer.x ·˙=RmaVecMulNN
cramer.q ×˙=/rR
Assertion cramerlem2 RCRingXBYVDXUnitRzVX·˙z=Yz=iNDXNmatRepVRYi×˙DX

Proof

Step Hyp Ref Expression
1 cramer.a A=NMatR
2 cramer.b B=BaseA
3 cramer.v V=BaseRN
4 cramer.d D=NmaDetR
5 cramer.x ·˙=RmaVecMulNN
6 cramer.q ×˙=/rR
7 simpll1 RCRingXBYVDXUnitRzVX·˙z=YRCRing
8 simpll2 RCRingXBYVDXUnitRzVX·˙z=YXBYV
9 simpll3 RCRingXBYVDXUnitRzVX·˙z=YDXUnitR
10 simplr RCRingXBYVDXUnitRzVX·˙z=YzV
11 simpr RCRingXBYVDXUnitRzVX·˙z=YX·˙z=Y
12 1 2 3 4 5 6 cramerlem1 RCRingXBYVDXUnitRzVX·˙z=Yz=iNDXNmatRepVRYi×˙DX
13 7 8 9 10 11 12 syl113anc RCRingXBYVDXUnitRzVX·˙z=Yz=iNDXNmatRepVRYi×˙DX
14 13 ex RCRingXBYVDXUnitRzVX·˙z=Yz=iNDXNmatRepVRYi×˙DX
15 14 ralrimiva RCRingXBYVDXUnitRzVX·˙z=Yz=iNDXNmatRepVRYi×˙DX