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	1 2	pmatring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ Ring )
14	3	matring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
15	4	ply1ring	⊢ ( 𝐴 ∈ Ring → 𝑄 ∈ Ring )
16	14 15	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑄 ∈ Ring )
17	7 11	isrim	⊢ ( ( 𝐶 ∈ Ring ∧ 𝑄 ∈ Ring ) → ( 𝑇 ∈ ( 𝐶 RingIso 𝑄 ) ↔ ( 𝑇 ∈ ( 𝐶 RingHom 𝑄 ) ∧ 𝑇 : ( Base ‘ 𝐶 ) –1-1-onto→ ( Base ‘ 𝑄 ) ) ) )
18	13 16 17	syl2anc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑇 ∈ ( 𝐶 RingIso 𝑄 ) ↔ ( 𝑇 ∈ ( 𝐶 RingHom 𝑄 ) ∧ 𝑇 : ( Base ‘ 𝐶 ) –1-1-onto→ ( Base ‘ 𝑄 ) ) ) )
19	6 12 18	mpbir2and	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 ∈ ( 𝐶 RingIso 𝑄 ) )