Theorem pm2mpgrpiso

Description: The transformation of polynomial matrices into polynomials over matrices is an additive group isomorphism. (Contributed by AV, 17-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	pm2mpgrpiso	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to T\in \left(C\mathrm{GrpIso}Q\right)$$

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 9 10	pm2mpghm	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to T\in \left(C\mathrm{GrpHom}Q\right)$$
12		eqid	$$⊢{\mathrm{Base}}_Q={\mathrm{Base}}_Q$$
13	1 2 3 4 5 6 7 8 12 10	pm2mpf1o	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to T:B\underset{1-1\; onto}{⟶}{\mathrm{Base}}_Q$$
14	3 12	isgim	$$⊢T\in \left(C\mathrm{GrpIso}Q\right)\leftrightarrow \left(T\in \left(C\mathrm{GrpHom}Q\right)\wedge T:B\underset{1-1\; onto}{⟶}{\mathrm{Base}}_Q\right)$$
15	11 13 14	sylanbrc	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to T\in \left(C\mathrm{GrpIso}Q\right)$$