m2cpmghm

Description: The transformation of matrices into constant polynomial matrices is an additive group 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	m2cpmghm	$⊢ (N \in Fin \land R \in Ring) \to T \in (A GrpHom 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		eqid	$⊢ {Base}_{C} = {Base}_{C}$
9	2 3 4 5 6 8	mat2pmatghm	$⊢ (N \in Fin \land R \in Ring) \to T \in (A GrpHom C)$
10	1 5 6	cpmatsubgpmat	$⊢ (N \in Fin \land R \in Ring) \to S \in SubGrp (C)$
11	1 2 3 4	m2cpmf	$⊢ (N \in Fin \land R \in Ring) \to T : B ⟶ S$
12	11	frnd	$⊢ (N \in Fin \land R \in Ring) \to ran T \subseteq S$
13	7	resghm2b	$⊢ (S \in SubGrp (C) \land ran T \subseteq S) \to (T \in (A GrpHom C) \leftrightarrow T \in (A GrpHom U))$
14	13	bicomd	$⊢ (S \in SubGrp (C) \land ran T \subseteq S) \to (T \in (A GrpHom U) \leftrightarrow T \in (A GrpHom C))$
15	10 12 14	syl2anc	$⊢ (N \in Fin \land R \in Ring) \to (T \in (A GrpHom U) \leftrightarrow T \in (A GrpHom C))$
16	9 15	mpbird	$⊢ (N \in Fin \land R \in Ring) \to T \in (A GrpHom U)$

Metamath Proof Explorer