m2cpmrhm

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

	Ref	Expression
Hypotheses	m2cpm.s	$⊢ S = N ConstPolyMat R$
	m2cpm.t	$⊢ T = N matToPolyMat R$
	m2cpm.a	$⊢ A = N Mat R$
	m2cpm.b	$⊢ B = {Base}_{A}$
	m2cpmghm.p	$⊢ P = {Poly}_{1} (R)$
	m2cpmghm.c	$⊢ C = N Mat P$
	m2cpmghm.u	$⊢ U = C ↾_{𝑠} S$
Assertion	m2cpmrhm	$⊢ (N \in Fin \land R \in CRing) \to T \in (A RingHom U)$

Step	Hyp	Ref	Expression
1		m2cpm.s	$⊢ S = N ConstPolyMat R$
2		m2cpm.t	$⊢ T = N matToPolyMat R$
3		m2cpm.a	$⊢ A = N Mat R$
4		m2cpm.b	$⊢ B = {Base}_{A}$
5		m2cpmghm.p	$⊢ P = {Poly}_{1} (R)$
6		m2cpmghm.c	$⊢ C = N Mat P$
7		m2cpmghm.u	$⊢ U = C ↾_{𝑠} S$
8		crngring	$⊢ R \in CRing \to R \in Ring$
9	3	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
10	8 9	sylan2	$⊢ (N \in Fin \land R \in CRing) \to A \in Ring$
11	1 5 6	cpmatsrgpmat	$⊢ (N \in Fin \land R \in Ring) \to S \in SubRing (C)$
12	8 11	sylan2	$⊢ (N \in Fin \land R \in CRing) \to S \in SubRing (C)$
13	7	subrgring	$⊢ S \in SubRing (C) \to U \in Ring$
14	12 13	syl	$⊢ (N \in Fin \land R \in CRing) \to U \in Ring$
15	1 2 3 4 5 6 7	m2cpmghm	$⊢ (N \in Fin \land R \in Ring) \to T \in (A GrpHom U)$
16	8 15	sylan2	$⊢ (N \in Fin \land R \in CRing) \to T \in (A GrpHom U)$
17	1 2 3 4 5 6 7	m2cpmmhm	$⊢ (N \in Fin \land R \in CRing) \to T \in ({mulGrp}_{A} MndHom {mulGrp}_{U})$
18	16 17	jca	$⊢ (N \in Fin \land R \in CRing) \to (T \in (A GrpHom U) \land T \in ({mulGrp}_{A} MndHom {mulGrp}_{U}))$
19		eqid	$⊢ {mulGrp}_{A} = {mulGrp}_{A}$
20		eqid	$⊢ {mulGrp}_{U} = {mulGrp}_{U}$
21	19 20	isrhm	$⊢ T \in (A RingHom U) \leftrightarrow ((A \in Ring \land U \in Ring) \land (T \in (A GrpHom U) \land T \in ({mulGrp}_{A} MndHom {mulGrp}_{U})))$
22	10 14 18 21	syl21anbrc	$⊢ (N \in Fin \land R \in CRing) \to T \in (A RingHom U)$

Metamath Proof Explorer