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	1 2	pmatring	|- ( ( N e. Fin /\ R e. Ring ) -> C e. Ring )
14	3	matring	|- ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
15	4	ply1ring	|- ( A e. Ring -> Q e. Ring )
16	14 15	syl	|- ( ( N e. Fin /\ R e. Ring ) -> Q e. Ring )
17	7 11	isrim	|- ( ( C e. Ring /\ Q e. Ring ) -> ( T e. ( C RingIso Q ) <-> ( T e. ( C RingHom Q ) /\ T : ( Base ` C ) -1-1-onto-> ( Base ` Q ) ) ) )
18	13 16 17	syl2anc	|- ( ( N e. Fin /\ R e. Ring ) -> ( T e. ( C RingIso Q ) <-> ( T e. ( C RingHom Q ) /\ T : ( Base ` C ) -1-1-onto-> ( Base ` Q ) ) ) )
19	6 12 18	mpbir2and	|- ( ( N e. Fin /\ R e. Ring ) -> T e. ( C RingIso Q ) )