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	|- S = ( N ConstPolyMat R )
	0elcpmat.p	|- P = ( Poly1 ` R )
	0elcpmat.c	|- C = ( N Mat P )
Assertion	0elcpmat	|- ( ( N e. Fin /\ R e. Ring ) -> ( 0g ` C ) e. S )

Proof

Step	Hyp	Ref	Expression
1		0elcpmat.s	|- S = ( N ConstPolyMat R )
2		0elcpmat.p	|- P = ( Poly1 ` R )
3		0elcpmat.c	|- C = ( N Mat P )
4	1 2 3	cpmatsubgpmat	|- ( ( N e. Fin /\ R e. Ring ) -> S e. ( SubGrp ` C ) )
5		eqid	|- ( 0g ` C ) = ( 0g ` C )
6	5	subg0cl	|- ( S e. ( SubGrp ` C ) -> ( 0g ` C ) e. S )
7	4 6	syl	|- ( ( N e. Fin /\ R e. Ring ) -> ( 0g ` C ) e. S )