Theorem 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 = ( Poly1 ` R )
	0mat2pmat.0	|- .0. = ( 0g ` ( N Mat R ) )
	0mat2pmat.z	|- Z = ( 0g ` ( N Mat P ) )
Assertion	0mat2pmat	|- ( ( R e. Ring /\ N e. Fin ) -> ( T ` .0. ) = Z )

Proof

Step	Hyp	Ref	Expression
1		idmatidpmat.t	|- T = ( N matToPolyMat R )
2		idmatidpmat.p	|- P = ( Poly1 ` R )
3		0mat2pmat.0	|- .0. = ( 0g ` ( N Mat R ) )
4		0mat2pmat.z	|- Z = ( 0g ` ( 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 e. Fin /\ R e. Ring ) -> T e. ( ( N Mat R ) GrpHom ( N Mat P ) ) )
10	9	ancoms	|- ( ( R e. Ring /\ N e. Fin ) -> T e. ( ( N Mat R ) GrpHom ( N Mat P ) ) )
11	3 4	ghmid	|- ( T e. ( ( N Mat R ) GrpHom ( N Mat P ) ) -> ( T ` .0. ) = Z )
12	10 11	syl	|- ( ( R e. Ring /\ N e. Fin ) -> ( T ` .0. ) = Z )