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 ) = 𝐼 ) |