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 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
idmatidpmat.p 𝑃 = ( Poly1𝑅 )
idmatidpmat.1 1 = ( 1r ‘ ( 𝑁 Mat 𝑅 ) )
idmatidpmat.i 𝐼 = ( 1r ‘ ( 𝑁 Mat 𝑃 ) )
Assertion idmatidpmat ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → ( 𝑇1 ) = 𝐼 )

Proof

Step Hyp Ref Expression
1 idmatidpmat.t 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
2 idmatidpmat.p 𝑃 = ( Poly1𝑅 )
3 idmatidpmat.1 1 = ( 1r ‘ ( 𝑁 Mat 𝑅 ) )
4 idmatidpmat.i 𝐼 = ( 1r ‘ ( 𝑁 Mat 𝑃 ) )
5 eqid ( 𝑁 Mat 𝑅 ) = ( 𝑁 Mat 𝑅 )
6 eqid ( Base ‘ ( 𝑁 Mat 𝑅 ) ) = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
7 eqid ( 𝑁 Mat 𝑃 ) = ( 𝑁 Mat 𝑃 )
8 eqid ( Base ‘ ( 𝑁 Mat 𝑃 ) ) = ( Base ‘ ( 𝑁 Mat 𝑃 ) )
9 1 5 6 2 7 8 mat2pmat1 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑇 ‘ ( 1r ‘ ( 𝑁 Mat 𝑅 ) ) ) = ( 1r ‘ ( 𝑁 Mat 𝑃 ) ) )
10 3 fveq2i ( 𝑇1 ) = ( 𝑇 ‘ ( 1r ‘ ( 𝑁 Mat 𝑅 ) ) )
11 9 10 4 3eqtr4g ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑇1 ) = 𝐼 )
12 11 ancoms ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → ( 𝑇1 ) = 𝐼 )