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	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	pm2mpmhm.c	$$⊢C=N\mathrm{Mat}P$$
	pm2mpmhm.a	$$⊢A=N\mathrm{Mat}R$$
	pm2mpmhm.q	$$⊢Q={\mathrm{Poly}}_1\left(A\right)$$
	pm2mpmhm.t	$$⊢T=N\mathrm{pMatToMatPoly}R$$
Assertion	pm2mprngiso	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to T\in \left(C\mathrm{RingIso}Q\right)$$

Proof

Step	Hyp	Ref	Expression
1		pm2mpmhm.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		pm2mpmhm.c	$$⊢C=N\mathrm{Mat}P$$
3		pm2mpmhm.a	$$⊢A=N\mathrm{Mat}R$$
4		pm2mpmhm.q	$$⊢Q={\mathrm{Poly}}_1\left(A\right)$$
5		pm2mpmhm.t	$$⊢T=N\mathrm{pMatToMatPoly}R$$
6	1 2 3 4 5	pm2mprhm	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to T\in \left(C\mathrm{RingHom}Q\right)$$
7		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
8		eqid	$$⊢{\cdot }_Q={\cdot }_Q$$
9		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_Q}={\cdot }_{{\mathrm{mulGrp}}_Q}$$
10		eqid	$$⊢{\mathrm{var}}_1\left(A\right)={\mathrm{var}}_1\left(A\right)$$
11		eqid	$$⊢{\mathrm{Base}}_Q={\mathrm{Base}}_Q$$
12	1 2 7 8 9 10 3 4 11 5	pm2mpf1o	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to T:{\mathrm{Base}}_C\underset{1-1\; onto}{⟶}{\mathrm{Base}}_Q$$
13	7 11	isrim	$$⊢T\in \left(C\mathrm{RingIso}Q\right)\leftrightarrow \left(T\in \left(C\mathrm{RingHom}Q\right)\wedge T:{\mathrm{Base}}_C\underset{1-1\; onto}{⟶}{\mathrm{Base}}_Q\right)$$
14	6 12 13	sylanbrc	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to T\in \left(C\mathrm{RingIso}Q\right)$$