Theorem 0elcpmat

Description: The zero of the ring of all polynomial matrices over the ring R is a constant polynomial matrix. (Contributed by AV, 27-Nov-2019)

	Ref	Expression
Hypotheses	0elcpmat.s	⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
	0elcpmat.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
	0elcpmat.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
Assertion	0elcpmat	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 0g ‘ 𝐶 ) ∈ 𝑆 )

Proof

Step	Hyp	Ref	Expression
1		0elcpmat.s	⊢ 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
2		0elcpmat.p	⊢ 𝑃 = ( Poly1 ‘ 𝑅 )
3		0elcpmat.c	⊢ 𝐶 = ( 𝑁 Mat 𝑃 )
4	1 2 3	cpmatsubgpmat	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ∈ ( SubGrp ‘ 𝐶 ) )
5		eqid	⊢ ( 0g ‘ 𝐶 ) = ( 0g ‘ 𝐶 )
6	5	subg0cl	⊢ ( 𝑆 ∈ ( SubGrp ‘ 𝐶 ) → ( 0g ‘ 𝐶 ) ∈ 𝑆 )
7	4 6	syl	⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 0g ‘ 𝐶 ) ∈ 𝑆 )