Metamath Proof Explorer

Theorem cpmatsubgpmat

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

Ref Expression
Hypotheses cpmatsrngpmat.s ⊢ S = N ConstPolyMat R
cpmatsrngpmat.p ⊢ P = Poly 1 ⁡ R
cpmatsrngpmat.c ⊢ C = N Mat P
Assertion cpmatsubgpmat ⊢ N ∈ Fin ∧ R ∈ Ring → S ∈ SubGrp ⁡ 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 eqid ⊢ Base C = Base C
5 1 2 3 4 cpmat ⊢ N ∈ Fin ∧ R ∈ Ring → S = m ∈ Base C | ∀ i ∈ N ∀ j ∈ N ∀ k ∈ ℕ coe 1 ⁡ i m j ⁡ k = 0 R
6 ssrab2 ⊢ m ∈ Base C | ∀ i ∈ N ∀ j ∈ N ∀ k ∈ ℕ coe 1 ⁡ i m j ⁡ k = 0 R ⊆ Base C
7 5 6 eqsstrdi ⊢ N ∈ Fin ∧ R ∈ Ring → S ⊆ Base C
8 1 2 3 1elcpmat ⊢ N ∈ Fin ∧ R ∈ Ring → 1 C ∈ S
9 8 ne0d ⊢ N ∈ Fin ∧ R ∈ Ring → S ≠ ∅
10 1 2 3 cpmatacl ⊢ N ∈ Fin ∧ R ∈ Ring → ∀ x ∈ S ∀ y ∈ S x + C y ∈ S
11 1 2 3 cpmatinvcl ⊢ N ∈ Fin ∧ R ∈ Ring → ∀ x ∈ S inv g ⁡ C ⁡ x ∈ S
12 r19.26 ⊢ ∀ x ∈ S ∀ y ∈ S x + C y ∈ S ∧ inv g ⁡ C ⁡ x ∈ S ↔ ∀ x ∈ S ∀ y ∈ S x + C y ∈ S ∧ ∀ x ∈ S inv g ⁡ C ⁡ x ∈ S
13 10 11 12 sylanbrc ⊢ N ∈ Fin ∧ R ∈ Ring → ∀ x ∈ S ∀ y ∈ S x + C y ∈ S ∧ inv g ⁡ C ⁡ x ∈ S
14 2 3 pmatring ⊢ N ∈ Fin ∧ R ∈ Ring → C ∈ Ring
15 ringgrp ⊢ C ∈ Ring → C ∈ Grp
16 eqid ⊢ + C = + C
17 eqid ⊢ inv g ⁡ C = inv g ⁡ C
18 4 16 17 issubg2 ⊢ C ∈ Grp → S ∈ SubGrp ⁡ C ↔ S ⊆ Base C ∧ S ≠ ∅ ∧ ∀ x ∈ S ∀ y ∈ S x + C y ∈ S ∧ inv g ⁡ C ⁡ x ∈ S
19 14 15 18 3syl ⊢ N ∈ Fin ∧ R ∈ Ring → S ∈ SubGrp ⁡ C ↔ S ⊆ Base C ∧ S ≠ ∅ ∧ ∀ x ∈ S ∀ y ∈ S x + C y ∈ S ∧ inv g ⁡ C ⁡ x ∈ S
20 7 9 13 19 mpbir3and ⊢ N ∈ Fin ∧ R ∈ Ring → S ∈ SubGrp ⁡ C