Description: The set of polynomial matrices over a ring is a ring. (Contributed by AV, 6-Nov-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | pmatring.p | ⊢ 𝑃 = ( Poly_{1} ‘ 𝑅 ) | |
pmatring.c | ⊢ 𝐶 = ( 𝑁 Mat 𝑃 ) | ||
Assertion | pmatring | ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ Ring ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | pmatring.p | ⊢ 𝑃 = ( Poly_{1} ‘ 𝑅 ) | |
2 | pmatring.c | ⊢ 𝐶 = ( 𝑁 Mat 𝑃 ) | |
3 | 1 | ply1ring | ⊢ ( 𝑅 ∈ Ring → 𝑃 ∈ Ring ) |
4 | 2 | matring | ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑃 ∈ Ring ) → 𝐶 ∈ Ring ) |
5 | 3 4 | sylan2 | ⊢ ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ Ring ) |