Step |
Hyp |
Ref |
Expression |
1 |
|
pm2mpmhm.p |
⊢ 𝑃 = ( Poly1 ‘ 𝑅 ) |
2 |
|
pm2mpmhm.c |
⊢ 𝐶 = ( 𝑁 Mat 𝑃 ) |
3 |
|
pm2mpmhm.a |
⊢ 𝐴 = ( 𝑁 Mat 𝑅 ) |
4 |
|
pm2mpmhm.q |
⊢ 𝑄 = ( Poly1 ‘ 𝐴 ) |
5 |
|
pm2mpmhm.t |
⊢ 𝑇 = ( 𝑁 pMatToMatPoly 𝑅 ) |
6 |
1 2 3 4 5
|
pm2mprhm |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 ∈ ( 𝐶 RingHom 𝑄 ) ) |
7 |
|
eqid |
⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 ) |
8 |
|
eqid |
⊢ ( ·𝑠 ‘ 𝑄 ) = ( ·𝑠 ‘ 𝑄 ) |
9 |
|
eqid |
⊢ ( .g ‘ ( mulGrp ‘ 𝑄 ) ) = ( .g ‘ ( mulGrp ‘ 𝑄 ) ) |
10 |
|
eqid |
⊢ ( var1 ‘ 𝐴 ) = ( var1 ‘ 𝐴 ) |
11 |
|
eqid |
⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 ) |
12 |
1 2 7 8 9 10 3 4 11 5
|
pm2mpf1o |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 : ( Base ‘ 𝐶 ) –1-1-onto→ ( Base ‘ 𝑄 ) ) |
13 |
7 11
|
isrim |
⊢ ( 𝑇 ∈ ( 𝐶 RingIso 𝑄 ) ↔ ( 𝑇 ∈ ( 𝐶 RingHom 𝑄 ) ∧ 𝑇 : ( Base ‘ 𝐶 ) –1-1-onto→ ( Base ‘ 𝑄 ) ) ) |
14 |
6 12 13
|
sylanbrc |
⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 ∈ ( 𝐶 RingIso 𝑄 ) ) |