Theorem pm2mpfo

Description: The transformation of polynomial matrices into polynomials over matrices is a function mapping polynomial matrices onto polynomials over matrices. (Contributed by AV, 12-Oct-2019) (Revised by AV, 6-Dec-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	pm2mpfo	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to T:B\underset{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	pm2mpf	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to T:B⟶L$$
12		eqid	$$⊢{\cdot }_P={\cdot }_P$$
13		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_P}={\cdot }_{{\mathrm{mulGrp}}_P}$$
14		eqid	$$⊢{\mathrm{var}}_1\left(R\right)={\mathrm{var}}_1\left(R\right)$$
15		eqid	$$⊢\left(l\in L⟼\left(i\in N,j\in N⟼\underset{k\in {\mathbb{N}}_0}{{\sum }_P}\left(\left(i{\mathrm{coe}}_1\left(l\right)\left(k\right)j\right){\cdot }_P\left(k{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\right)\right)\right)\right)=\left(l\in L⟼\left(i\in N,j\in N⟼\underset{k\in {\mathbb{N}}_0}{{\sum }_P}\left(\left(i{\mathrm{coe}}_1\left(l\right)\left(k\right)j\right){\cdot }_P\left(k{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\right)\right)\right)\right)$$
16	7 8 9 12 13 14 15 1 10	mp2pm2mp	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\wedge p\in L\right)\to T\left(\left(l\in L⟼\left(i\in N,j\in N⟼\underset{k\in {\mathbb{N}}_0}{{\sum }_P}\left(\left(i{\mathrm{coe}}_1\left(l\right)\left(k\right)j\right){\cdot }_P\left(k{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\right)\right)\right)\right)\left(p\right)\right)=p$$
17	16	3expa	$$⊢\left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\wedge p\in L\right)\to T\left(\left(l\in L⟼\left(i\in N,j\in N⟼\underset{k\in {\mathbb{N}}_0}{{\sum }_P}\left(\left(i{\mathrm{coe}}_1\left(l\right)\left(k\right)j\right){\cdot }_P\left(k{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\right)\right)\right)\right)\left(p\right)\right)=p$$
18	7 8 9 1 12 13 14 15 2 3	mply1topmatcl	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\wedge p\in L\right)\to \left(l\in L⟼\left(i\in N,j\in N⟼\underset{k\in {\mathbb{N}}_0}{{\sum }_P}\left(\left(i{\mathrm{coe}}_1\left(l\right)\left(k\right)j\right){\cdot }_P\left(k{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\right)\right)\right)\right)\left(p\right)\in B$$
19	18	3expa	$$⊢\left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\wedge p\in L\right)\to \left(l\in L⟼\left(i\in N,j\in N⟼\underset{k\in {\mathbb{N}}_0}{{\sum }_P}\left(\left(i{\mathrm{coe}}_1\left(l\right)\left(k\right)j\right){\cdot }_P\left(k{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\right)\right)\right)\right)\left(p\right)\in B$$
20		simpr	$$⊢\left(\left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\wedge p\in L\right)\wedge f=\left(l\in L⟼\left(i\in N,j\in N⟼\underset{k\in {\mathbb{N}}_0}{{\sum }_P}\left(\left(i{\mathrm{coe}}_1\left(l\right)\left(k\right)j\right){\cdot }_P\left(k{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\right)\right)\right)\right)\left(p\right)\right)\to f=\left(l\in L⟼\left(i\in N,j\in N⟼\underset{k\in {\mathbb{N}}_0}{{\sum }_P}\left(\left(i{\mathrm{coe}}_1\left(l\right)\left(k\right)j\right){\cdot }_P\left(k{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\right)\right)\right)\right)\left(p\right)$$
21	20	fveq2d	$$⊢\left(\left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\wedge p\in L\right)\wedge f=\left(l\in L⟼\left(i\in N,j\in N⟼\underset{k\in {\mathbb{N}}_0}{{\sum }_P}\left(\left(i{\mathrm{coe}}_1\left(l\right)\left(k\right)j\right){\cdot }_P\left(k{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\right)\right)\right)\right)\left(p\right)\right)\to T\left(f\right)=T\left(\left(l\in L⟼\left(i\in N,j\in N⟼\underset{k\in {\mathbb{N}}_0}{{\sum }_P}\left(\left(i{\mathrm{coe}}_1\left(l\right)\left(k\right)j\right){\cdot }_P\left(k{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\right)\right)\right)\right)\left(p\right)\right)$$
22	21	eqeq2d	$$⊢\left(\left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\wedge p\in L\right)\wedge f=\left(l\in L⟼\left(i\in N,j\in N⟼\underset{k\in {\mathbb{N}}_0}{{\sum }_P}\left(\left(i{\mathrm{coe}}_1\left(l\right)\left(k\right)j\right){\cdot }_P\left(k{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\right)\right)\right)\right)\left(p\right)\right)\to \left(p=T\left(f\right)\leftrightarrow p=T\left(\left(l\in L⟼\left(i\in N,j\in N⟼\underset{k\in {\mathbb{N}}_0}{{\sum }_P}\left(\left(i{\mathrm{coe}}_1\left(l\right)\left(k\right)j\right){\cdot }_P\left(k{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\right)\right)\right)\right)\left(p\right)\right)\right)$$
23	19 22	rspcedv	$$⊢\left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\wedge p\in L\right)\to \left(p=T\left(\left(l\in L⟼\left(i\in N,j\in N⟼\underset{k\in {\mathbb{N}}_0}{{\sum }_P}\left(\left(i{\mathrm{coe}}_1\left(l\right)\left(k\right)j\right){\cdot }_P\left(k{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\right)\right)\right)\right)\left(p\right)\right)\to \exists f\in Bp=T\left(f\right)\right)$$
24	23	com12	$$⊢p=T\left(\left(l\in L⟼\left(i\in N,j\in N⟼\underset{k\in {\mathbb{N}}_0}{{\sum }_P}\left(\left(i{\mathrm{coe}}_1\left(l\right)\left(k\right)j\right){\cdot }_P\left(k{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\right)\right)\right)\right)\left(p\right)\right)\to \left(\left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\wedge p\in L\right)\to \exists f\in Bp=T\left(f\right)\right)$$
25	24	eqcoms	$$⊢T\left(\left(l\in L⟼\left(i\in N,j\in N⟼\underset{k\in {\mathbb{N}}_0}{{\sum }_P}\left(\left(i{\mathrm{coe}}_1\left(l\right)\left(k\right)j\right){\cdot }_P\left(k{\cdot }_{{\mathrm{mulGrp}}_P}{\mathrm{var}}_1\left(R\right)\right)\right)\right)\right)\left(p\right)\right)=p\to \left(\left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\wedge p\in L\right)\to \exists f\in Bp=T\left(f\right)\right)$$
26	17 25	mpcom	$$⊢\left(\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\wedge p\in L\right)\to \exists f\in Bp=T\left(f\right)$$
27	26	ralrimiva	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to \forall p\in L\exists f\in Bp=T\left(f\right)$$
28		dffo3	$$⊢T:B\underset{onto}{⟶}L\leftrightarrow \left(T:B⟶L\wedge \forall p\in L\exists f\in Bp=T\left(f\right)\right)$$
29	11 27 28	sylanbrc	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to T:B\underset{onto}{⟶}L$$