mat2pmatrhm

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

	Ref	Expression
Hypotheses	mat2pmatbas.t	$⊢ T = N matToPolyMat R$
	mat2pmatbas.a	$⊢ A = N Mat R$
	mat2pmatbas.b	$⊢ B = {Base}_{A}$
	mat2pmatbas.p	$⊢ P = {Poly}_{1} (R)$
	mat2pmatbas.c	$⊢ C = N Mat P$
	mat2pmatbas0.h	$⊢ H = {Base}_{C}$
Assertion	mat2pmatrhm	$⊢ (N \in Fin \land R \in CRing) \to T \in (A RingHom C)$

Step	Hyp	Ref	Expression
1		mat2pmatbas.t	$⊢ T = N matToPolyMat R$
2		mat2pmatbas.a	$⊢ A = N Mat R$
3		mat2pmatbas.b	$⊢ B = {Base}_{A}$
4		mat2pmatbas.p	$⊢ P = {Poly}_{1} (R)$
5		mat2pmatbas.c	$⊢ C = N Mat P$
6		mat2pmatbas0.h	$⊢ H = {Base}_{C}$
7		crngring	$⊢ R \in CRing \to R \in Ring$
8	2	matring	$⊢ (N \in Fin \land R \in Ring) \to A \in Ring$
9	7 8	sylan2	$⊢ (N \in Fin \land R \in CRing) \to A \in Ring$
10	4	ply1ring	$⊢ R \in Ring \to P \in Ring$
11	7 10	syl	$⊢ R \in CRing \to P \in Ring$
12	5	matring	$⊢ (N \in Fin \land P \in Ring) \to C \in Ring$
13	11 12	sylan2	$⊢ (N \in Fin \land R \in CRing) \to C \in Ring$
14	1 2 3 4 5 6	mat2pmatghm	$⊢ (N \in Fin \land R \in Ring) \to T \in (A GrpHom C)$
15	7 14	sylan2	$⊢ (N \in Fin \land R \in CRing) \to T \in (A GrpHom C)$
16	1 2 3 4 5 6	mat2pmatmhm	$⊢ (N \in Fin \land R \in CRing) \to T \in ({mulGrp}_{A} MndHom {mulGrp}_{C})$
17	15 16	jca	$⊢ (N \in Fin \land R \in CRing) \to (T \in (A GrpHom C) \land T \in ({mulGrp}_{A} MndHom {mulGrp}_{C}))$
18		eqid	$⊢ {mulGrp}_{A} = {mulGrp}_{A}$
19		eqid	$⊢ {mulGrp}_{C} = {mulGrp}_{C}$
20	18 19	isrhm	$⊢ T \in (A RingHom C) \leftrightarrow ((A \in Ring \land C \in Ring) \land (T \in (A GrpHom C) \land T \in ({mulGrp}_{A} MndHom {mulGrp}_{C})))$
21	9 13 17 20	syl21anbrc	$⊢ (N \in Fin \land R \in CRing) \to T \in (A RingHom C)$

Metamath Proof Explorer