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	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
	idmatidpmat.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	0mat2pmat.0	⊢ 0 = ( 0g ‘ ( 𝑁 Mat 𝑅 ) )
	0mat2pmat.z	⊢ 𝑍 = ( 0g ‘ ( 𝑁 Mat 𝑃 ) )
Assertion	0mat2pmat	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → ( 𝑇 ‘ 0 ) = 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		idmatidpmat.t	⊢ 𝑇 = ( 𝑁 matToPolyMat 𝑅 )
2		idmatidpmat.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		0mat2pmat.0	⊢ 0 = ( 0g ‘ ( 𝑁 Mat 𝑅 ) )
4		0mat2pmat.z	⊢ 𝑍 = ( 0g ‘ ( 𝑁 Mat 𝑃 ) )
5		eqid	⊢ ( 𝑁 Mat 𝑅 ) = ( 𝑁 Mat 𝑅 )
6		eqid	⊢ ( Base ‘ ( 𝑁 Mat 𝑅 ) ) = ( Base ‘ ( 𝑁 Mat 𝑅 ) )
7		eqid	⊢ ( 𝑁 Mat 𝑃 ) = ( 𝑁 Mat 𝑃 )
8		eqid	⊢ ( Base ‘ ( 𝑁 Mat 𝑃 ) ) = ( Base ‘ ( 𝑁 Mat 𝑃 ) )
9	1 5 6 2 7 8	mat2pmatghm	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑇 ∈ ( ( 𝑁 Mat 𝑅 ) GrpHom ( 𝑁 Mat 𝑃 ) ) )
10	9	ancoms	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → 𝑇 ∈ ( ( 𝑁 Mat 𝑅 ) GrpHom ( 𝑁 Mat 𝑃 ) ) )
11	3 4	ghmid	⊢ ( 𝑇 ∈ ( ( 𝑁 Mat 𝑅 ) GrpHom ( 𝑁 Mat 𝑃 ) ) → ( 𝑇 ‘ 0 ) = 𝑍 )
12	10 11	syl	⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ Fin ) → ( 𝑇 ‘ 0 ) = 𝑍 )