0mat2pmat

Description: The transformed zero matrix is the zero polynomial matrix. (Contributed by AV, 5-Aug-2019) (Proof shortened by AV, 19-Nov-2019)

	Ref	Expression
Hypotheses	idmatidpmat.t	$⊢ T = N matToPolyMat R$
	idmatidpmat.p	$⊢ P = {Poly}_{1} (R)$
	0mat2pmat.0	$⊢ \underset{˙}{0} = 0_{(N Mat R)}$
	0mat2pmat.z	$⊢ Z = 0_{(N Mat P)}$
Assertion	0mat2pmat	$⊢ (R \in Ring \land N \in Fin) \to T (\underset{˙}{0}) = Z$

Step	Hyp	Ref	Expression
1		idmatidpmat.t	$⊢ T = N matToPolyMat R$
2		idmatidpmat.p	$⊢ P = {Poly}_{1} (R)$
3		0mat2pmat.0	$⊢ \underset{˙}{0} = 0_{(N Mat R)}$
4		0mat2pmat.z	$⊢ Z = 0_{(N Mat P)}$
5		eqid	$⊢ N Mat R = N Mat R$
6		eqid	$⊢ {Base}_{(N Mat R)} = {Base}_{(N Mat R)}$
7		eqid	$⊢ N Mat P = N Mat P$
8		eqid	$⊢ {Base}_{(N Mat P)} = {Base}_{(N Mat P)}$
9	1 5 6 2 7 8	mat2pmatghm	$⊢ (N \in Fin \land R \in Ring) \to T \in ((N Mat R) GrpHom (N Mat P))$
10	9	ancoms	$⊢ (R \in Ring \land N \in Fin) \to T \in ((N Mat R) GrpHom (N Mat P))$
11	3 4	ghmid	$⊢ T \in ((N Mat R) GrpHom (N Mat P)) \to T (\underset{˙}{0}) = Z$
12	10 11	syl	$⊢ (R \in Ring \land N \in Fin) \to T (\underset{˙}{0}) = Z$

Metamath Proof Explorer