Step |
Hyp |
Ref |
Expression |
1 |
|
pm2mpmhm.p |
|- P = ( Poly1 ` R ) |
2 |
|
pm2mpmhm.c |
|- C = ( N Mat P ) |
3 |
|
pm2mpmhm.a |
|- A = ( N Mat R ) |
4 |
|
pm2mpmhm.q |
|- Q = ( Poly1 ` A ) |
5 |
|
pm2mpmhm.t |
|- T = ( N pMatToMatPoly R ) |
6 |
1 2 3 4 5
|
pm2mprhm |
|- ( ( N e. Fin /\ R e. Ring ) -> T e. ( C RingHom Q ) ) |
7 |
|
eqid |
|- ( Base ` C ) = ( Base ` C ) |
8 |
|
eqid |
|- ( .s ` Q ) = ( .s ` Q ) |
9 |
|
eqid |
|- ( .g ` ( mulGrp ` Q ) ) = ( .g ` ( mulGrp ` Q ) ) |
10 |
|
eqid |
|- ( var1 ` A ) = ( var1 ` A ) |
11 |
|
eqid |
|- ( Base ` Q ) = ( Base ` Q ) |
12 |
1 2 7 8 9 10 3 4 11 5
|
pm2mpf1o |
|- ( ( N e. Fin /\ R e. Ring ) -> T : ( Base ` C ) -1-1-onto-> ( Base ` Q ) ) |
13 |
7 11
|
isrim |
|- ( T e. ( C RingIso Q ) <-> ( T e. ( C RingHom Q ) /\ T : ( Base ` C ) -1-1-onto-> ( Base ` Q ) ) ) |
14 |
6 12 13
|
sylanbrc |
|- ( ( N e. Fin /\ R e. Ring ) -> T e. ( C RingIso Q ) ) |