Metamath Proof Explorer


Theorem pm2mprngiso

Description: The transformation of polynomial matrices into polynomials over matrices is a ring isomorphism. (Contributed by AV, 22-Oct-2019)

Ref Expression
Hypotheses pm2mpmhm.p 𝑃 = ( Poly1𝑅 )
pm2mpmhm.c 𝐶 = ( 𝑁 Mat 𝑃 )
pm2mpmhm.a 𝐴 = ( 𝑁 Mat 𝑅 )
pm2mpmhm.q 𝑄 = ( Poly1𝐴 )
pm2mpmhm.t 𝑇 = ( 𝑁 pMatToMatPoly 𝑅 )
Assertion pm2mprngiso ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 ∈ ( 𝐶 RingIso 𝑄 ) )

Proof

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 𝑄 ) )