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=NConstPolyMatR
cpmatsrngpmat.p ⊢P=Poly1⁡R
cpmatsrngpmat.c ⊢C=NMatP
Assertion cpmatsubgpmat ⊢N∈Fin∧R∈Ring→S∈SubGrp⁡C

Proof

Step Hyp Ref Expression
1 cpmatsrngpmat.s ⊢S=NConstPolyMatR
2 cpmatsrngpmat.p ⊢P=Poly1⁡R
3 cpmatsrngpmat.c ⊢C=NMatP
4 eqid ⊢BaseC=BaseC
5 1 2 3 4 cpmat ⊢N∈Fin∧R∈Ring→S=m∈BaseC|∀i∈N∀j∈N∀k∈ℕcoe1⁡imj⁡k=0R
6 ssrab2 ⊢m∈BaseC|∀i∈N∀j∈N∀k∈ℕcoe1⁡imj⁡k=0R⊆BaseC
7 5 6 eqsstrdi ⊢N∈Fin∧R∈Ring→S⊆BaseC
8 1 2 3 1elcpmat ⊢N∈Fin∧R∈Ring→1C∈S
9 8 ne0d ⊢N∈Fin∧R∈Ring→S≠∅
10 1 2 3 cpmatacl ⊢N∈Fin∧R∈Ring→∀x∈S∀y∈Sx+Cy∈S
11 1 2 3 cpmatinvcl ⊢N∈Fin∧R∈Ring→∀x∈Sinvg⁡C⁡x∈S
12 r19.26 ⊢∀x∈S∀y∈Sx+Cy∈S∧invg⁡C⁡x∈S↔∀x∈S∀y∈Sx+Cy∈S∧∀x∈Sinvg⁡C⁡x∈S
13 10 11 12 sylanbrc ⊢N∈Fin∧R∈Ring→∀x∈S∀y∈Sx+Cy∈S∧invg⁡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 ⊢invg⁡C=invg⁡C
18 4 16 17 issubg2 ⊢C∈Grp→S∈SubGrp⁡C↔S⊆BaseC∧S≠∅∧∀x∈S∀y∈Sx+Cy∈S∧invg⁡C⁡x∈S
19 14 15 18 3syl ⊢N∈Fin∧R∈Ring→S∈SubGrp⁡C↔S⊆BaseC∧S≠∅∧∀x∈S∀y∈Sx+Cy∈S∧invg⁡C⁡x∈S
20 7 9 13 19 mpbir3and ⊢N∈Fin∧R∈Ring→S∈SubGrp⁡C