Theorem mat2pmatrhm

Description: The transformation of matrices into polynomial matrices is a ring homomorphism. (Contributed by AV, 29-Oct-2019)

	Ref	Expression
Hypotheses	mat2pmatbas.t	|- T = ( N matToPolyMat R )
	mat2pmatbas.a	|- A = ( N Mat R )
	mat2pmatbas.b	|- B = ( Base ` A )
	mat2pmatbas.p	|- P = ( Poly1 ` R )
	mat2pmatbas.c	|- C = ( N Mat P )
	mat2pmatbas0.h	|- H = ( Base ` C )
Assertion	mat2pmatrhm	|- ( ( N e. Fin /\ R e. CRing ) -> T e. ( A RingHom C ) )

Proof

Step	Hyp	Ref	Expression
1		mat2pmatbas.t	|- T = ( N matToPolyMat R )
2		mat2pmatbas.a	|- A = ( N Mat R )
3		mat2pmatbas.b	|- B = ( Base ` A )
4		mat2pmatbas.p	|- P = ( Poly1 ` R )
5		mat2pmatbas.c	|- C = ( N Mat P )
6		mat2pmatbas0.h	|- H = ( Base ` C )
7		crngring	|- ( R e. CRing -> R e. Ring )
8	2	matring	|- ( ( N e. Fin /\ R e. Ring ) -> A e. Ring )
9	7 8	sylan2	|- ( ( N e. Fin /\ R e. CRing ) -> A e. Ring )
10	4	ply1ring	|- ( R e. Ring -> P e. Ring )
11	7 10	syl	|- ( R e. CRing -> P e. Ring )
12	5	matring	|- ( ( N e. Fin /\ P e. Ring ) -> C e. Ring )
13	11 12	sylan2	|- ( ( N e. Fin /\ R e. CRing ) -> C e. Ring )
14	1 2 3 4 5 6	mat2pmatghm	|- ( ( N e. Fin /\ R e. Ring ) -> T e. ( A GrpHom C ) )
15	7 14	sylan2	|- ( ( N e. Fin /\ R e. CRing ) -> T e. ( A GrpHom C ) )
16	1 2 3 4 5 6	mat2pmatmhm	|- ( ( N e. Fin /\ R e. CRing ) -> T e. ( ( mulGrp ` A ) MndHom ( mulGrp ` C ) ) )
17	15 16	jca	|- ( ( N e. Fin /\ R e. CRing ) -> ( T e. ( A GrpHom C ) /\ T e. ( ( mulGrp ` A ) MndHom ( mulGrp ` C ) ) ) )
18		eqid	|- ( mulGrp ` A ) = ( mulGrp ` A )
19		eqid	|- ( mulGrp ` C ) = ( mulGrp ` C )
20	18 19	isrhm	|- ( T e. ( A RingHom C ) <-> ( ( A e. Ring /\ C e. Ring ) /\ ( T e. ( A GrpHom C ) /\ T e. ( ( mulGrp ` A ) MndHom ( mulGrp ` C ) ) ) ) )
21	9 13 17 20	syl21anbrc	|- ( ( N e. Fin /\ R e. CRing ) -> T e. ( A RingHom C ) )