Description: The transformation of matrices into constant polynomial matrices is a homomorphism of multiplicative monoids. (Contributed by AV, 18-Nov-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | m2cpm.s | |
|
m2cpm.t | |
||
m2cpm.a | |
||
m2cpm.b | |
||
m2cpmghm.p | |
||
m2cpmghm.c | |
||
m2cpmghm.u | |
||
Assertion | m2cpmmhm | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | m2cpm.s | |
|
2 | m2cpm.t | |
|
3 | m2cpm.a | |
|
4 | m2cpm.b | |
|
5 | m2cpmghm.p | |
|
6 | m2cpmghm.c | |
|
7 | m2cpmghm.u | |
|
8 | eqid | |
|
9 | 2 3 4 5 6 8 | mat2pmatmhm | |
10 | crngring | |
|
11 | 10 | anim2i | |
12 | 1 5 6 | cpmatsrgpmat | |
13 | eqid | |
|
14 | 13 | subrgsubm | |
15 | 11 12 14 | 3syl | |
16 | 1 2 3 4 | m2cpmf | |
17 | frn | |
|
18 | 11 16 17 | 3syl | |
19 | 6 | ovexi | |
20 | 1 | ovexi | |
21 | 7 13 | mgpress | |
22 | 19 20 21 | mp2an | |
23 | 22 | eqcomi | |
24 | 23 | resmhm2b | |
25 | 15 18 24 | syl2anc | |
26 | 9 25 | mpbid | |