Description: The transformation of polynomial matrices into polynomials over matrices is an additive group isomorphism. (Contributed by AV, 17-Oct-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | pm2mpfo.p | |
|
pm2mpfo.c | |
||
pm2mpfo.b | |
||
pm2mpfo.m | |
||
pm2mpfo.e | |
||
pm2mpfo.x | |
||
pm2mpfo.a | |
||
pm2mpfo.q | |
||
pm2mpfo.l | |
||
pm2mpfo.t | |
||
Assertion | pm2mpgrpiso | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pm2mpfo.p | |
|
2 | pm2mpfo.c | |
|
3 | pm2mpfo.b | |
|
4 | pm2mpfo.m | |
|
5 | pm2mpfo.e | |
|
6 | pm2mpfo.x | |
|
7 | pm2mpfo.a | |
|
8 | pm2mpfo.q | |
|
9 | pm2mpfo.l | |
|
10 | pm2mpfo.t | |
|
11 | 1 2 3 4 5 6 7 8 9 10 | pm2mpghm | |
12 | eqid | |
|
13 | 1 2 3 4 5 6 7 8 12 10 | pm2mpf1o | |
14 | 3 12 | isgim | |
15 | 11 13 14 | sylanbrc | |