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 = ( Poly1 ` R )
	pm2mpfo.c	|- C = ( N Mat P )
	pm2mpfo.b	|- B = ( Base ` C )
	pm2mpfo.m	|- .* = ( .s ` Q )
	pm2mpfo.e	|- .^ = ( .g ` ( mulGrp ` Q ) )
	pm2mpfo.x	|- X = ( var1 ` A )
	pm2mpfo.a	|- A = ( N Mat R )
	pm2mpfo.q	|- Q = ( Poly1 ` A )
	pm2mpfo.l	|- L = ( Base ` Q )
	pm2mpfo.t	|- T = ( N pMatToMatPoly R )
Assertion	pm2mpgrpiso	|- ( ( N e. Fin /\ R e. Ring ) -> T e. ( C GrpIso Q ) )

Proof

Step	Hyp	Ref	Expression
1		pm2mpfo.p	|- P = ( Poly1 ` R )
2		pm2mpfo.c	|- C = ( N Mat P )
3		pm2mpfo.b	|- B = ( Base ` C )
4		pm2mpfo.m	|- .* = ( .s ` Q )
5		pm2mpfo.e	|- .^ = ( .g ` ( mulGrp ` Q ) )
6		pm2mpfo.x	|- X = ( var1 ` A )
7		pm2mpfo.a	|- A = ( N Mat R )
8		pm2mpfo.q	|- Q = ( Poly1 ` A )
9		pm2mpfo.l	|- L = ( Base ` Q )
10		pm2mpfo.t	|- T = ( N pMatToMatPoly R )
11	1 2 3 4 5 6 7 8 9 10	pm2mpghm	|- ( ( N e. Fin /\ R e. Ring ) -> T e. ( C GrpHom Q ) )
12		eqid	|- ( Base ` Q ) = ( Base ` Q )
13	1 2 3 4 5 6 7 8 12 10	pm2mpf1o	|- ( ( N e. Fin /\ R e. Ring ) -> T : B -1-1-onto-> ( Base ` Q ) )
14	3 12	isgim	|- ( T e. ( C GrpIso Q ) <-> ( T e. ( C GrpHom Q ) /\ T : B -1-1-onto-> ( Base ` Q ) ) )
15	11 13 14	sylanbrc	|- ( ( N e. Fin /\ R e. Ring ) -> T e. ( C GrpIso Q ) )