Metamath Proof Explorer


Theorem idmatidpmat

Description: The transformed identity matrix is the identity polynomial matrix. (Contributed by AV, 1-Aug-2019) (Proof shortened by AV, 19-Nov-2019)

Ref Expression
Hypotheses idmatidpmat.t
|- T = ( N matToPolyMat R )
idmatidpmat.p
|- P = ( Poly1 ` R )
idmatidpmat.1
|- .1. = ( 1r ` ( N Mat R ) )
idmatidpmat.i
|- I = ( 1r ` ( N Mat P ) )
Assertion idmatidpmat
|- ( ( R e. Ring /\ N e. Fin ) -> ( T ` .1. ) = I )

Proof

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 )