Metamath Proof Explorer

Theorem cpmatsrgpmat

Description: The set of all constant polynomial matrices over a ring R is a subring of the ring of all polynomial matrices over the ring R . (Contributed by AV, 18-Nov-2019)

Ref Expression
Hypotheses cpmatsrngpmat.s ⊢ S = N ConstPolyMat R
cpmatsrngpmat.p ⊢ P = Poly 1 ⁡ R
cpmatsrngpmat.c ⊢ C = N Mat P
Assertion cpmatsrgpmat ⊢ N ∈ Fin ∧ R ∈ Ring → S ∈ SubRing ⁡ C

Proof

Step Hyp Ref Expression
1 cpmatsrngpmat.s ⊢ S = N ConstPolyMat R
2 cpmatsrngpmat.p ⊢ P = Poly 1 ⁡ R
3 cpmatsrngpmat.c ⊢ C = N Mat P
4 1 2 3 cpmatsubgpmat ⊢ N ∈ Fin ∧ R ∈ Ring → S ∈ SubGrp ⁡ C
5 1 2 3 1elcpmat ⊢ N ∈ Fin ∧ R ∈ Ring → 1 C ∈ S
6 1 2 3 cpmatmcl ⊢ N ∈ Fin ∧ R ∈ Ring → ∀ x ∈ S ∀ y ∈ S x ⋅ C y ∈ S
7 2 3 pmatring ⊢ N ∈ Fin ∧ R ∈ Ring → C ∈ Ring
8 eqid ⊢ Base C = Base C
9 eqid ⊢ 1 C = 1 C
10 eqid ⊢ ⋅ C = ⋅ C
11 8 9 10 issubrg2 ⊢ C ∈ Ring → S ∈ SubRing ⁡ C ↔ S ∈ SubGrp ⁡ C ∧ 1 C ∈ S ∧ ∀ x ∈ S ∀ y ∈ S x ⋅ C y ∈ S
12 7 11 syl ⊢ N ∈ Fin ∧ R ∈ Ring → S ∈ SubRing ⁡ C ↔ S ∈ SubGrp ⁡ C ∧ 1 C ∈ S ∧ ∀ x ∈ S ∀ y ∈ S x ⋅ C y ∈ S
13 4 5 6 12 mpbir3and ⊢ N ∈ Fin ∧ R ∈ Ring → S ∈ SubRing ⁡ C