Description: The set of polynomial matrices over a ring is a ring. (Contributed by AV, 6Nov2019)
Ref  Expression  

Hypotheses  pmatring.p   P = ( Poly1 ` R ) 

pmatring.c   C = ( N Mat P ) 

Assertion  pmatring   ( ( N e. Fin /\ R e. Ring ) > C e. Ring ) 
Step  Hyp  Ref  Expression 

1  pmatring.p   P = ( Poly1 ` R ) 

2  pmatring.c   C = ( N Mat P ) 

3  1  ply1ring   ( R e. Ring > P e. Ring ) 
4  2  matring   ( ( N e. Fin /\ P e. Ring ) > C e. Ring ) 
5  3 4  sylan2   ( ( N e. Fin /\ R e. Ring ) > C e. Ring ) 