Step |
Hyp |
Ref |
Expression |
1 |
|
idmatidpmat.t |
|- T = ( N matToPolyMat R ) |
2 |
|
idmatidpmat.p |
|- P = ( Poly1 ` R ) |
3 |
|
idmatidpmat.1 |
|- .1. = ( 1r ` ( N Mat R ) ) |
4 |
|
idmatidpmat.i |
|- I = ( 1r ` ( N Mat P ) ) |
5 |
|
eqid |
|- ( N Mat R ) = ( N Mat R ) |
6 |
|
eqid |
|- ( Base ` ( N Mat R ) ) = ( Base ` ( N Mat R ) ) |
7 |
|
eqid |
|- ( N Mat P ) = ( N Mat P ) |
8 |
|
eqid |
|- ( Base ` ( N Mat P ) ) = ( Base ` ( N Mat P ) ) |
9 |
1 5 6 2 7 8
|
mat2pmat1 |
|- ( ( N e. Fin /\ R e. Ring ) -> ( T ` ( 1r ` ( N Mat R ) ) ) = ( 1r ` ( N Mat P ) ) ) |
10 |
3
|
fveq2i |
|- ( T ` .1. ) = ( T ` ( 1r ` ( N Mat R ) ) ) |
11 |
9 10 4
|
3eqtr4g |
|- ( ( N e. Fin /\ R e. Ring ) -> ( T ` .1. ) = I ) |
12 |
11
|
ancoms |
|- ( ( R e. Ring /\ N e. Fin ) -> ( T ` .1. ) = I ) |