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	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
	mat2pmatbas.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	mat2pmatbas.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	mat2pmatbas.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	mat2pmatbas.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	mat2pmatbas0.h	⊢ 𝐻 = ( Base ‘ 𝐶 )
Assertion	mat2pmatrhm	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑇 ∈ ( 𝐴 RingHom 𝐶 ) )

Proof

Step	Hyp	Ref	Expression
1		mat2pmatbas.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
2		mat2pmatbas.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
3		mat2pmatbas.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
4		mat2pmatbas.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
5		mat2pmatbas.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
6		mat2pmatbas0.h	⊢ 𝐻 = ( Base ‘ 𝐶 )
7		crngring	⊢ ( 𝑅 ∈ CRing → 𝑅 ∈ Ring )
8	2	matring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
9	7 8	sylan2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐴 ∈ Ring )
10	4	ply1ring	⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
11	7 10	syl	⊢ ( 𝑅 ∈ CRing → 𝑃 ∈ Ring )
12	5	matring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) → 𝐶 ∈ Ring )
13	11 12	sylan2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝐶 ∈ Ring )
14	1 2 3 4 5 6	mat2pmatghm	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 ∈ ( 𝐴 GrpHom 𝐶 ) )
15	7 14	sylan2	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑇 ∈ ( 𝐴 GrpHom 𝐶 ) )
16	1 2 3 4 5 6	mat2pmatmhm	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑇 ∈ ( ( mulGrp ‘ 𝐴 ) MndHom ( mulGrp ‘ 𝐶 ) ) )
17	15 16	jca	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → ( 𝑇 ∈ ( 𝐴 GrpHom 𝐶 ) ∧ 𝑇 ∈ ( ( mulGrp ‘ 𝐴 ) MndHom ( mulGrp ‘ 𝐶 ) ) ) )
18		eqid	⊢ ( mulGrp ‘ 𝐴 ) = ( mulGrp ‘ 𝐴 )
19		eqid	⊢ ( mulGrp ‘ 𝐶 ) = ( mulGrp ‘ 𝐶 )
20	18 19	isrhm	⊢ ( 𝑇 ∈ ( 𝐴 RingHom 𝐶 ) ↔ ( ( 𝐴 ∈ Ring ∧ 𝐶 ∈ Ring ) ∧ ( 𝑇 ∈ ( 𝐴 GrpHom 𝐶 ) ∧ 𝑇 ∈ ( ( mulGrp ‘ 𝐴 ) MndHom ( mulGrp ‘ 𝐶 ) ) ) ) )
21	9 13 17 20	syl21anbrc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ CRing ) → 𝑇 ∈ ( 𝐴 RingHom 𝐶 ) )