Theorem pm2mpmhm

Description: The transformation of polynomial matrices into polynomials over matrices is a homomorphism of multiplicative monoids. (Contributed by AV, 22-Oct-2019) (Revised by AV, 6-Dec-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	pm2mpmhm	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to T\in \left({\mathrm{mulGrp}}_C\mathrm{MndHom}{\mathrm{mulGrp}}_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	pmatring	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to C\in \mathrm{Ring}$$
7		eqid	$$⊢{\mathrm{mulGrp}}_C={\mathrm{mulGrp}}_C$$
8	7	ringmgp	$$⊢C\in \mathrm{Ring}\to {\mathrm{mulGrp}}_C\in \mathrm{Mnd}$$
9	6 8	syl	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to {\mathrm{mulGrp}}_C\in \mathrm{Mnd}$$
10	3	matring	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to A\in \mathrm{Ring}$$
11	4	ply1ring	$$⊢A\in \mathrm{Ring}\to Q\in \mathrm{Ring}$$
12		eqid	$$⊢{\mathrm{mulGrp}}_Q={\mathrm{mulGrp}}_Q$$
13	12	ringmgp	$$⊢Q\in \mathrm{Ring}\to {\mathrm{mulGrp}}_Q\in \mathrm{Mnd}$$
14	10 11 13	3syl	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to {\mathrm{mulGrp}}_Q\in \mathrm{Mnd}$$
15		eqid	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_C$$
16	7 15	mgpbas	$$⊢{\mathrm{Base}}_C={\mathrm{Base}}_{{\mathrm{mulGrp}}_C}$$
17	16	eqcomi	$$⊢{\mathrm{Base}}_{{\mathrm{mulGrp}}_C}={\mathrm{Base}}_C$$
18		eqid	$$⊢{\cdot }_Q={\cdot }_Q$$
19		eqid	$$⊢{\cdot }_{{\mathrm{mulGrp}}_Q}={\cdot }_{{\mathrm{mulGrp}}_Q}$$
20		eqid	$$⊢{\mathrm{var}}_1\left(A\right)={\mathrm{var}}_1\left(A\right)$$
21		eqid	$$⊢{\mathrm{Base}}_Q={\mathrm{Base}}_Q$$
22	12 21	mgpbas	$$⊢{\mathrm{Base}}_Q={\mathrm{Base}}_{{\mathrm{mulGrp}}_Q}$$
23	22	eqcomi	$$⊢{\mathrm{Base}}_{{\mathrm{mulGrp}}_Q}={\mathrm{Base}}_Q$$
24	1 2 17 18 19 20 3 4 5 23	pm2mpf	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to T:{\mathrm{Base}}_{{\mathrm{mulGrp}}_C}⟶{\mathrm{Base}}_{{\mathrm{mulGrp}}_Q}$$
25	1 2 3 4 5 17	pm2mpmhmlem2	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to \forall x\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_C}\forall y\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_C}T\left(x{\cdot }_{C}y\right)=T\left(x\right){\cdot }_{Q}T\left(y\right)$$
26	1 2 15 18 19 20 3 4 5	idpm2idmp	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to T\left(1_C\right)=1_Q$$
27	24 25 26	3jca	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to \left(T:{\mathrm{Base}}_{{\mathrm{mulGrp}}_C}⟶{\mathrm{Base}}_{{\mathrm{mulGrp}}_Q}\wedge \forall x\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_C}\forall y\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_C}T\left(x{\cdot }_{C}y\right)=T\left(x\right){\cdot }_{Q}T\left(y\right)\wedge T\left(1_C\right)=1_Q\right)$$
28		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{mulGrp}}_C}={\mathrm{Base}}_{{\mathrm{mulGrp}}_C}$$
29		eqid	$$⊢{\mathrm{Base}}_{{\mathrm{mulGrp}}_Q}={\mathrm{Base}}_{{\mathrm{mulGrp}}_Q}$$
30		eqid	$$⊢{\cdot }_C={\cdot }_C$$
31	7 30	mgpplusg	$$⊢{\cdot }_C={+}_{{\mathrm{mulGrp}}_C}$$
32		eqid	$$⊢{\cdot }_Q={\cdot }_Q$$
33	12 32	mgpplusg	$$⊢{\cdot }_Q={+}_{{\mathrm{mulGrp}}_Q}$$
34		eqid	$$⊢1_C=1_C$$
35	7 34	ringidval	$$⊢1_C=0_{{\mathrm{mulGrp}}_C}$$
36		eqid	$$⊢1_Q=1_Q$$
37	12 36	ringidval	$$⊢1_Q=0_{{\mathrm{mulGrp}}_Q}$$
38	28 29 31 33 35 37	ismhm	$$⊢T\in \left({\mathrm{mulGrp}}_C\mathrm{MndHom}{\mathrm{mulGrp}}_Q\right)\leftrightarrow \left(\left({\mathrm{mulGrp}}_C\in \mathrm{Mnd}\wedge {\mathrm{mulGrp}}_Q\in \mathrm{Mnd}\right)\wedge \left(T:{\mathrm{Base}}_{{\mathrm{mulGrp}}_C}⟶{\mathrm{Base}}_{{\mathrm{mulGrp}}_Q}\wedge \forall x\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_C}\forall y\in {\mathrm{Base}}_{{\mathrm{mulGrp}}_C}T\left(x{\cdot }_{C}y\right)=T\left(x\right){\cdot }_{Q}T\left(y\right)\wedge T\left(1_C\right)=1_Q\right)\right)$$
39	9 14 27 38	syl21anbrc	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to T\in \left({\mathrm{mulGrp}}_C\mathrm{MndHom}{\mathrm{mulGrp}}_Q\right)$$