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\mathrm{ConstPolyMat}R$$
	0elcpmat.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
	0elcpmat.c	$$⊢C=N\mathrm{Mat}P$$
Assertion	0elcpmat	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to 0_C\in S$$

Proof

Step	Hyp	Ref	Expression
1		0elcpmat.s	$$⊢S=N\mathrm{ConstPolyMat}R$$
2		0elcpmat.p	$$⊢P={\mathrm{Poly}}_1\left(R\right)$$
3		0elcpmat.c	$$⊢C=N\mathrm{Mat}P$$
4	1 2 3	cpmatsubgpmat	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to S\in \mathrm{SubGrp}\left(C\right)$$
5		eqid	$$⊢0_C=0_C$$
6	5	subg0cl	$$⊢S\in \mathrm{SubGrp}\left(C\right)\to 0_C\in S$$
7	4 6	syl	$$⊢\left(N\in \mathrm{Fin}\wedge R\in \mathrm{Ring}\right)\to 0_C\in S$$