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	$⊢ P = {Poly}_{1} (R)$
	pm2mpmhm.c	$⊢ C = N Mat P$
	pm2mpmhm.a	$⊢ A = N Mat R$
	pm2mpmhm.q	$⊢ Q = {Poly}_{1} (A)$
	pm2mpmhm.t	$⊢ T = N pMatToMatPoly R$
Assertion	pm2mprhm	$⊢ (N \in Fin \land R \in Ring) \to T \in (C RingHom Q)$

Step	Hyp	Ref	Expression
1		pm2mpmhm.p	$⊢ P = {Poly}_{1} (R)$
2		pm2mpmhm.c	$⊢ C = N Mat P$
3		pm2mpmhm.a	$⊢ A = N Mat R$
4		pm2mpmhm.q	$⊢ Q = {Poly}_{1} (A)$
5		pm2mpmhm.t	$⊢ T = N pMatToMatPoly R$
6	1 2	pmatring	$⊢ (N \in Fin \land R \in Ring) \to C \in Ring$
7	3	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
8	4	ply1ring	$⊢ A \in Ring \to Q \in Ring$
9	7 8	syl	$⊢ (N \in Fin \land R \in Ring) \to Q \in Ring$
10		eqid	$⊢ {Base}_{C} = {Base}_{C}$
11		eqid	$⊢ \cdot_{Q} = \cdot_{Q}$
12		eqid	$⊢ \cdot_{{mulGrp}_{Q}} = \cdot_{{mulGrp}_{Q}}$
13		eqid	$⊢ {var}_{1} (A) = {var}_{1} (A)$
14		eqid	$⊢ {Base}_{Q} = {Base}_{Q}$
15	1 2 10 11 12 13 3 4 14 5	pm2mpghm	$⊢ (N \in Fin \land R \in Ring) \to T \in (C GrpHom Q)$
16	1 2 3 4 5	pm2mpmhm	$⊢ (N \in Fin \land R \in Ring) \to T \in ({mulGrp}_{C} MndHom {mulGrp}_{Q})$
17	15 16	jca	$⊢ (N \in Fin \land R \in Ring) \to (T \in (C GrpHom Q) \land T \in ({mulGrp}_{C} MndHom {mulGrp}_{Q}))$
18		eqid	$⊢ {mulGrp}_{C} = {mulGrp}_{C}$
19		eqid	$⊢ {mulGrp}_{Q} = {mulGrp}_{Q}$
20	18 19	isrhm	$⊢ T \in (C RingHom Q) \leftrightarrow ((C \in Ring \land Q \in Ring) \land (T \in (C GrpHom Q) \land T \in ({mulGrp}_{C} MndHom {mulGrp}_{Q})))$
21	6 9 17 20	syl21anbrc	$⊢ (N \in Fin \land R \in Ring) \to T \in (C RingHom Q)$

Metamath Proof Explorer