Metamath Proof Explorer


Theorem pmatring

Description: The set of polynomial matrices over a ring is a ring. (Contributed by AV, 6-Nov-2019)

Ref Expression
Hypotheses pmatring.p 𝑃 = ( Poly1𝑅 )
pmatring.c 𝐶 = ( 𝑁 Mat 𝑃 )
Assertion pmatring ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ Ring )

Proof

Step Hyp Ref Expression
1 pmatring.p 𝑃 = ( Poly1𝑅 )
2 pmatring.c 𝐶 = ( 𝑁 Mat 𝑃 )
3 1 ply1ring ( 𝑅 ∈ Ring → 𝑃 ∈ Ring )
4 2 matring ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) → 𝐶 ∈ Ring )
5 3 4 sylan2 ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ Ring )