Metamath Proof Explorer

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	$⊢ P = {Poly}_{1} (R)$
		pmmpric.c	$⊢ C = N Mat P$
		pmmpric.a	$⊢ A = N Mat R$
		pmmpric.q	$⊢ Q = {Poly}_{1} (A)$
	Assertion	pmmpric	$⊢ (N \in Fin \land R \in Ring) \to C ≃_{𝑟} Q$

Proof

Step	Hyp	Ref	Expression
1		pmmpric.p	$⊢ P = {Poly}_{1} (R)$
2		pmmpric.c	$⊢ C = N Mat P$
3		pmmpric.a	$⊢ A = N Mat R$
4		pmmpric.q	$⊢ Q = {Poly}_{1} (A)$
5		eqid	$⊢ N pMatToMatPoly R = N pMatToMatPoly R$
6	1 2 3 4 5	pm2mprngiso	$⊢ (N \in Fin \land R \in Ring) \to N pMatToMatPoly R \in (C RingIso Q)$
7	6	ne0d	$⊢ (N \in Fin \land R \in Ring) \to C RingIso Q \neq \emptyset$
8		brric	$⊢ C ≃_{𝑟} Q \leftrightarrow C RingIso Q \neq \emptyset$
9	7 8	sylibr	$⊢ (N \in Fin \land R \in Ring) \to C ≃_{𝑟} Q$