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