Step |
Hyp |
Ref |
Expression |
1 |
|
m2cpmfo.s |
|- S = ( N ConstPolyMat R ) |
2 |
|
m2cpmfo.t |
|- T = ( N matToPolyMat R ) |
3 |
|
m2cpmfo.a |
|- A = ( N Mat R ) |
4 |
|
m2cpmfo.k |
|- K = ( Base ` A ) |
5 |
|
m2cpmrngiso.p |
|- P = ( Poly1 ` R ) |
6 |
|
m2cpmrngiso.c |
|- C = ( N Mat P ) |
7 |
|
m2cpmrngiso.u |
|- U = ( C |`s S ) |
8 |
1 2 3 4 5 6 7
|
m2cpmrhm |
|- ( ( N e. Fin /\ R e. CRing ) -> T e. ( A RingHom U ) ) |
9 |
|
crngring |
|- ( R e. CRing -> R e. Ring ) |
10 |
1 2 3 4
|
m2cpmf1o |
|- ( ( N e. Fin /\ R e. Ring ) -> T : K -1-1-onto-> S ) |
11 |
|
eqid |
|- ( Base ` C ) = ( Base ` C ) |
12 |
1 5 6 11
|
cpmatpmat |
|- ( ( N e. Fin /\ R e. Ring /\ m e. S ) -> m e. ( Base ` C ) ) |
13 |
12
|
3expia |
|- ( ( N e. Fin /\ R e. Ring ) -> ( m e. S -> m e. ( Base ` C ) ) ) |
14 |
13
|
ssrdv |
|- ( ( N e. Fin /\ R e. Ring ) -> S C_ ( Base ` C ) ) |
15 |
7 11
|
ressbas2 |
|- ( S C_ ( Base ` C ) -> S = ( Base ` U ) ) |
16 |
14 15
|
syl |
|- ( ( N e. Fin /\ R e. Ring ) -> S = ( Base ` U ) ) |
17 |
16
|
eqcomd |
|- ( ( N e. Fin /\ R e. Ring ) -> ( Base ` U ) = S ) |
18 |
17
|
f1oeq3d |
|- ( ( N e. Fin /\ R e. Ring ) -> ( T : K -1-1-onto-> ( Base ` U ) <-> T : K -1-1-onto-> S ) ) |
19 |
10 18
|
mpbird |
|- ( ( N e. Fin /\ R e. Ring ) -> T : K -1-1-onto-> ( Base ` U ) ) |
20 |
9 19
|
sylan2 |
|- ( ( N e. Fin /\ R e. CRing ) -> T : K -1-1-onto-> ( Base ` U ) ) |
21 |
|
eqid |
|- ( Base ` U ) = ( Base ` U ) |
22 |
4 21
|
isrim |
|- ( T e. ( A RingIso U ) <-> ( T e. ( A RingHom U ) /\ T : K -1-1-onto-> ( Base ` U ) ) ) |
23 |
8 20 22
|
sylanbrc |
|- ( ( N e. Fin /\ R e. CRing ) -> T e. ( A RingIso U ) ) |