Metamath Proof Explorer


Theorem dmatscmcl

Description: The multiplication of a diagonal matrix with a scalar is a diagonal matrix. (Contributed by AV, 19-Dec-2019)

Ref Expression
Hypotheses dmatscmcl.k K=BaseR
dmatscmcl.a A=NMatR
dmatscmcl.b B=BaseA
dmatscmcl.s ˙=A
dmatscmcl.d D=NDMatR
Assertion dmatscmcl NFinRRingCKMDC˙MD

Proof

Step Hyp Ref Expression
1 dmatscmcl.k K=BaseR
2 dmatscmcl.a A=NMatR
3 dmatscmcl.b B=BaseA
4 dmatscmcl.s ˙=A
5 dmatscmcl.d D=NDMatR
6 simprl NFinRRingCKMDCK
7 eqid 0R=0R
8 2 3 7 5 dmatmat NFinRRingMDMB
9 8 com12 MDNFinRRingMB
10 9 adantl CKMDNFinRRingMB
11 10 impcom NFinRRingCKMDMB
12 6 11 jca NFinRRingCKMDCKMB
13 1 2 3 4 matvscl NFinRRingCKMBC˙MB
14 12 13 syldan NFinRRingCKMDC˙MB
15 2 3 7 5 dmatel NFinRRingMDMBiNjNijiMj=0R
16 15 adantr NFinRRingCKMDMBiNjNijiMj=0R
17 simp-4r NFinRRingCKMBiNjNRRing
18 simpr NFinRRingCKCK
19 18 anim1i NFinRRingCKMBCKMB
20 19 adantr NFinRRingCKMBiNjNCKMB
21 simpr NFinRRingCKMBiNjNiNjN
22 17 20 21 3jca NFinRRingCKMBiNjNRRingCKMBiNjN
23 22 adantr NFinRRingCKMBiNjNiMj=0RRRingCKMBiNjN
24 eqid R=R
25 2 3 1 4 24 matvscacell RRingCKMBiNjNiC˙Mj=CRiMj
26 23 25 syl NFinRRingCKMBiNjNiMj=0RiC˙Mj=CRiMj
27 oveq2 iMj=0RCRiMj=CR0R
28 27 adantl NFinRRingCKMBiNjNiMj=0RCRiMj=CR0R
29 1 24 7 ringrz RRingCKCR0R=0R
30 29 ad5ant23 NFinRRingCKMBiNjNCR0R=0R
31 30 adantr NFinRRingCKMBiNjNiMj=0RCR0R=0R
32 26 28 31 3eqtrd NFinRRingCKMBiNjNiMj=0RiC˙Mj=0R
33 32 ex NFinRRingCKMBiNjNiMj=0RiC˙Mj=0R
34 33 imim2d NFinRRingCKMBiNjNijiMj=0RijiC˙Mj=0R
35 34 ralimdvva NFinRRingCKMBiNjNijiMj=0RiNjNijiC˙Mj=0R
36 35 expimpd NFinRRingCKMBiNjNijiMj=0RiNjNijiC˙Mj=0R
37 16 36 sylbid NFinRRingCKMDiNjNijiC˙Mj=0R
38 37 impr NFinRRingCKMDiNjNijiC˙Mj=0R
39 2 3 7 5 dmatel NFinRRingC˙MDC˙MBiNjNijiC˙Mj=0R
40 39 adantr NFinRRingCKMDC˙MDC˙MBiNjNijiC˙Mj=0R
41 14 38 40 mpbir2and NFinRRingCKMDC˙MD