Description: The ring of polynomial matrices over a ring is isomorphic to the ring of polynomials over matrices of the same dimension over the same ring. (Contributed by AV, 30-Dec-2019)
| Ref | Expression | ||
|---|---|---|---|
| Hypotheses | pmmpric.p | |- P = ( Poly1 ` R ) |
|
| pmmpric.c | |- C = ( N Mat P ) |
||
| pmmpric.a | |- A = ( N Mat R ) |
||
| pmmpric.q | |- Q = ( Poly1 ` A ) |
||
| Assertion | pmmpric | |- ( ( N e. Fin /\ R e. Ring ) -> C ~=r Q ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pmmpric.p | |- P = ( Poly1 ` R ) |
|
| 2 | pmmpric.c | |- C = ( N Mat P ) |
|
| 3 | pmmpric.a | |- A = ( N Mat R ) |
|
| 4 | pmmpric.q | |- Q = ( Poly1 ` A ) |
|
| 5 | eqid | |- ( N pMatToMatPoly R ) = ( N pMatToMatPoly R ) |
|
| 6 | 1 2 3 4 5 | pm2mprngiso | |- ( ( N e. Fin /\ R e. Ring ) -> ( N pMatToMatPoly R ) e. ( C RingIso Q ) ) |
| 7 | 6 | ne0d | |- ( ( N e. Fin /\ R e. Ring ) -> ( C RingIso Q ) =/= (/) ) |
| 8 | brric | |- ( C ~=r Q <-> ( C RingIso Q ) =/= (/) ) |
|
| 9 | 7 8 | sylibr | |- ( ( N e. Fin /\ R e. Ring ) -> C ~=r Q ) |