Theorem pm2mprngiso

Description: The transformation of polynomial matrices into polynomials over matrices is a ring isomorphism. (Contributed by AV, 22-Oct-2019)

	Ref	Expression
Hypotheses	pm2mpmhm.p	|- P = ( Poly1 ` R )
	pm2mpmhm.c	|- C = ( N Mat P )
	pm2mpmhm.a	|- A = ( N Mat R )
	pm2mpmhm.q	|- Q = ( Poly1 ` A )
	pm2mpmhm.t	|- T = ( N pMatToMatPoly R )
Assertion	pm2mprngiso	|- ( ( N e. Fin /\ R e. Ring ) -> T e. ( C RingIso Q ) )

Proof

Step	Hyp	Ref	Expression
1		pm2mpmhm.p	|- P = ( Poly1 ` R )
2		pm2mpmhm.c	|- C = ( N Mat P )
3		pm2mpmhm.a	|- A = ( N Mat R )
4		pm2mpmhm.q	|- Q = ( Poly1 ` A )
5		pm2mpmhm.t	|- T = ( N pMatToMatPoly R )
6	1 2 3 4 5	pm2mprhm	|- ( ( N e. Fin /\ R e. Ring ) -> T e. ( C RingHom Q ) )
7		eqid	|- ( Base ` C ) = ( Base ` C )
8		eqid	|- ( .s ` Q ) = ( .s ` Q )
9		eqid	|- ( .g ` ( mulGrp ` Q ) ) = ( .g ` ( mulGrp ` Q ) )
10		eqid	|- ( var1 ` A ) = ( var1 ` A )
11		eqid	|- ( Base ` Q ) = ( Base ` Q )
12	1 2 7 8 9 10 3 4 11 5	pm2mpf1o	|- ( ( N e. Fin /\ R e. Ring ) -> T : ( Base ` C ) -1-1-onto-> ( Base ` Q ) )
13	7 11	isrim	|- ( T e. ( C RingIso Q ) <-> ( T e. ( C RingHom Q ) /\ T : ( Base ` C ) -1-1-onto-> ( Base ` Q ) ) )
14	6 12 13	sylanbrc	|- ( ( N e. Fin /\ R e. Ring ) -> T e. ( C RingIso Q ) )