Theorem pmmpric

Description: The ring of polynomial matrices over a ring is isomorphic to the ring of polynomials over matrices of the same dimension over the same ring. (Contributed by AV, 30-Dec-2019)

	Ref	Expression
Hypotheses	pmmpric.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	pmmpric.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	pmmpric.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	pmmpric.q	⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
Assertion	pmmpric	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ≃𝑟 𝑄 )

Proof

Step	Hyp	Ref	Expression
1		pmmpric.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		pmmpric.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3		pmmpric.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
4		pmmpric.q	⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
5		eqid	⊢ ( 𝑁 pMatToMatPoly 𝑅 ) = ( 𝑁 pMatToMatPoly 𝑅 )
6	1 2 3 4 5	pm2mprngiso	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑁 pMatToMatPoly 𝑅 ) ∈ ( 𝐶 RingIso 𝑄 ) )
7	6	ne0d	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝐶 RingIso 𝑄 ) ≠ ∅ )
8		brric	⊢ ( 𝐶 ≃𝑟 𝑄 ↔ ( 𝐶 RingIso 𝑄 ) ≠ ∅ )
9	7 8	sylibr	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ≃𝑟 𝑄 )