Theorem pm2mpf1o

Description: The transformation of polynomial matrices into polynomials over matrices is a 1-1 function mapping polynomial matrices onto polynomials over matrices. (Contributed by AV, 14-Oct-2019)

	Ref	Expression
Hypotheses	pm2mpfo.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	pm2mpfo.c	$$⊢C=N\mathrm{Mat}P$$
	pm2mpfo.b	$$⊢B={\mathrm{Base}}_C$$
	pm2mpfo.m	$$⊢\underset{\dot{}}{\ast }={\cdot }_Q$$
	pm2mpfo.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_Q}$$
	pm2mpfo.x	$$⊢X={\mathrm{var}}_1\left(A\right)$$
	pm2mpfo.a	$$⊢A=N\mathrm{Mat}R$$
	pm2mpfo.q	$$⊢Q={\mathrm{Poly}}_1\left(A\right)$$
	pm2mpfo.l	$$⊢L={\mathrm{Base}}_Q$$
	pm2mpfo.t	$$⊢T=N\mathrm{pMatToMatPoly}R$$
Assertion	pm2mpf1o	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to T:B\underset{1-1\; onto}{⟶}L$$

Proof

Step	Hyp	Ref	Expression
1		pm2mpfo.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
2		pm2mpfo.c	$$⊢C=N\mathrm{Mat}P$$
3		pm2mpfo.b	$$⊢B={\mathrm{Base}}_C$$
4		pm2mpfo.m	$$⊢\underset{\dot{}}{\ast }={\cdot }_Q$$
5		pm2mpfo.e	$$⊢\underset{\dot{}}{\times }={\cdot }_{{\mathrm{mulGrp}}_Q}$$
6		pm2mpfo.x	$$⊢X={\mathrm{var}}_1\left(A\right)$$
7		pm2mpfo.a	$$⊢A=N\mathrm{Mat}R$$
8		pm2mpfo.q	$$⊢Q={\mathrm{Poly}}_1\left(A\right)$$
9		pm2mpfo.l	$$⊢L={\mathrm{Base}}_Q$$
10		pm2mpfo.t	$$⊢T=N\mathrm{pMatToMatPoly}R$$
11	1 2 3 4 5 6 7 8 10 9	pm2mpf1	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to T:B\underset{1-1}{⟶}L$$
12	1 2 3 4 5 6 7 8 9 10	pm2mpfo	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to T:B\underset{onto}{⟶}L$$
13		df-f1o	$$⊢T:B\underset{1-1\; onto}{⟶}L\leftrightarrow \left(T:B\underset{1-1}{⟶}L\wedge T:B\underset{onto}{⟶}L\right)$$
14	11 12 13	sylanbrc	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to T:B\underset{1-1\; onto}{⟶}L$$