Theorem pm2mprhm

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

	Ref	Expression
Hypotheses	pm2mpmhm.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	pm2mpmhm.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
	pm2mpmhm.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	pm2mpmhm.q	⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
	pm2mpmhm.t	⊢ 𝑇 = ( 𝑁 pMatToMatPoly 𝑅 )
Assertion	pm2mprhm	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 ∈ ( 𝐶 RingHom 𝑄 ) )

Proof

Step	Hyp	Ref	Expression
1		pm2mpmhm.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
2		pm2mpmhm.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
3		pm2mpmhm.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
4		pm2mpmhm.q	⊢ 𝑄 = ( Poly1 ‘ 𝐴 )
5		pm2mpmhm.t	⊢ 𝑇 = ( 𝑁 pMatToMatPoly 𝑅 )
6	1 2	pmatring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ Ring )
7	3	matring	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐴 ∈ Ring )
8	4	ply1ring	⊢ ( 𝐴 ∈ Ring → 𝑄 ∈ Ring )
9	7 8	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑄 ∈ Ring )
10		eqid	⊢ ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
11		eqid	⊢ ( ·𝑠 ‘ 𝑄 ) = ( ·𝑠 ‘ 𝑄 )
12		eqid	⊢ ( .g ‘ ( mulGrp ‘ 𝑄 ) ) = ( .g ‘ ( mulGrp ‘ 𝑄 ) )
13		eqid	⊢ ( var1 ‘ 𝐴 ) = ( var1 ‘ 𝐴 )
14		eqid	⊢ ( Base ‘ 𝑄 ) = ( Base ‘ 𝑄 )
15	1 2 10 11 12 13 3 4 14 5	pm2mpghm	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 ∈ ( 𝐶 GrpHom 𝑄 ) )
16	1 2 3 4 5	pm2mpmhm	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 ∈ ( ( mulGrp ‘ 𝐶 ) MndHom ( mulGrp ‘ 𝑄 ) ) )
17	15 16	jca	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑇 ∈ ( 𝐶 GrpHom 𝑄 ) ∧ 𝑇 ∈ ( ( mulGrp ‘ 𝐶 ) MndHom ( mulGrp ‘ 𝑄 ) ) ) )
18		eqid	⊢ ( mulGrp ‘ 𝐶 ) = ( mulGrp ‘ 𝐶 )
19		eqid	⊢ ( mulGrp ‘ 𝑄 ) = ( mulGrp ‘ 𝑄 )
20	18 19	isrhm	⊢ ( 𝑇 ∈ ( 𝐶 RingHom 𝑄 ) ↔ ( ( 𝐶 ∈ Ring ∧ 𝑄 ∈ Ring ) ∧ ( 𝑇 ∈ ( 𝐶 GrpHom 𝑄 ) ∧ 𝑇 ∈ ( ( mulGrp ‘ 𝐶 ) MndHom ( mulGrp ‘ 𝑄 ) ) ) ) )
21	6 9 17 20	syl21anbrc	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 ∈ ( 𝐶 RingHom 𝑄 ) )