Theorem m2cpmrngiso

Description: The transformation of matrices into constant polynomial matrices is a ring isomorphism. (Contributed by AV, 19-Nov-2019)

	Ref	Expression
Hypotheses	m2cpmfo.s	|- S = ( N ConstPolyMat R )
	m2cpmfo.t	|- T = ( N matToPolyMat R )
	m2cpmfo.a	|- A = ( N Mat R )
	m2cpmfo.k	|- K = ( Base ` A )
	m2cpmrngiso.p	|- P = ( Poly1 ` R )
	m2cpmrngiso.c	|- C = ( N Mat P )
	m2cpmrngiso.u	|- U = ( C |`s S )
Assertion	m2cpmrngiso	|- ( ( N e. Fin /\ R e. CRing ) -> T e. ( A RingIso U ) )

Proof

Step	Hyp	Ref	Expression
1		m2cpmfo.s	|- S = ( N ConstPolyMat R )
2		m2cpmfo.t	|- T = ( N matToPolyMat R )
3		m2cpmfo.a	|- A = ( N Mat R )
4		m2cpmfo.k	|- K = ( Base ` A )
5		m2cpmrngiso.p	|- P = ( Poly1 ` R )
6		m2cpmrngiso.c	|- C = ( N Mat P )
7		m2cpmrngiso.u	|- U = ( C |`s S )
8	1 2 3 4 5 6 7	m2cpmrhm	|- ( ( N e. Fin /\ R e. CRing ) -> T e. ( A RingHom U ) )
9		crngring	|- ( R e. CRing -> R e. Ring )
10	1 2 3 4	m2cpmf1o	|- ( ( N e. Fin /\ R e. Ring ) -> T : K -1-1-onto-> S )
11		eqid	|- ( Base ` C ) = ( Base ` C )
12	1 5 6 11	cpmatpmat	|- ( ( N e. Fin /\ R e. Ring /\ m e. S ) -> m e. ( Base ` C ) )
13	12	3expia	|- ( ( N e. Fin /\ R e. Ring ) -> ( m e. S -> m e. ( Base ` C ) ) )
14	13	ssrdv	|- ( ( N e. Fin /\ R e. Ring ) -> S C_ ( Base ` C ) )
15	7 11	ressbas2	|- ( S C_ ( Base ` C ) -> S = ( Base ` U ) )
16	14 15	syl	|- ( ( N e. Fin /\ R e. Ring ) -> S = ( Base ` U ) )
17	16	eqcomd	|- ( ( N e. Fin /\ R e. Ring ) -> ( Base ` U ) = S )
18	17	f1oeq3d	|- ( ( N e. Fin /\ R e. Ring ) -> ( T : K -1-1-onto-> ( Base ` U ) <-> T : K -1-1-onto-> S ) )
19	10 18	mpbird	|- ( ( N e. Fin /\ R e. Ring ) -> T : K -1-1-onto-> ( Base ` U ) )
20	9 19	sylan2	|- ( ( N e. Fin /\ R e. CRing ) -> T : K -1-1-onto-> ( Base ` U ) )
21		eqid	|- ( Base ` U ) = ( Base ` U )
22	4 21	isrim	|- ( T e. ( A RingIso U ) <-> ( T e. ( A RingHom U ) /\ T : K -1-1-onto-> ( Base ` U ) ) )
23	8 20 22	sylanbrc	|- ( ( N e. Fin /\ R e. CRing ) -> T e. ( A RingIso U ) )