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 | |
|
dmatscmcl.a | |
||
dmatscmcl.b | |
||
dmatscmcl.s | |
||
dmatscmcl.d | |
||
Assertion | dmatscmcl | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | dmatscmcl.k | |
|
2 | dmatscmcl.a | |
|
3 | dmatscmcl.b | |
|
4 | dmatscmcl.s | |
|
5 | dmatscmcl.d | |
|
6 | simprl | |
|
7 | eqid | |
|
8 | 2 3 7 5 | dmatmat | |
9 | 8 | com12 | |
10 | 9 | adantl | |
11 | 10 | impcom | |
12 | 6 11 | jca | |
13 | 1 2 3 4 | matvscl | |
14 | 12 13 | syldan | |
15 | 2 3 7 5 | dmatel | |
16 | 15 | adantr | |
17 | simp-4r | |
|
18 | simpr | |
|
19 | 18 | anim1i | |
20 | 19 | adantr | |
21 | simpr | |
|
22 | 17 20 21 | 3jca | |
23 | 22 | adantr | |
24 | eqid | |
|
25 | 2 3 1 4 24 | matvscacell | |
26 | 23 25 | syl | |
27 | oveq2 | |
|
28 | 27 | adantl | |
29 | 1 24 7 | ringrz | |
30 | 29 | ad5ant23 | |
31 | 30 | adantr | |
32 | 26 28 31 | 3eqtrd | |
33 | 32 | ex | |
34 | 33 | imim2d | |
35 | 34 | ralimdvva | |
36 | 35 | expimpd | |
37 | 16 36 | sylbid | |
38 | 37 | impr | |
39 | 2 3 7 5 | dmatel | |
40 | 39 | adantr | |
41 | 14 38 40 | mpbir2and | |