Metamath Proof Explorer


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𝐶 ) ∈ 𝑆 )