# 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 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
cpmatsrngpmat.p 𝑃 = ( Poly1𝑅 )
cpmatsrngpmat.c 𝐶 = ( 𝑁 Mat 𝑃 )
Assertion cpmatsubgpmat ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ∈ ( SubGrp ‘ 𝐶 ) )

### Proof

Step Hyp Ref Expression
1 cpmatsrngpmat.s 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
2 cpmatsrngpmat.p 𝑃 = ( Poly1𝑅 )
3 cpmatsrngpmat.c 𝐶 = ( 𝑁 Mat 𝑃 )
4 eqid ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
5 1 2 3 4 cpmat ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 = { 𝑚 ∈ ( Base ‘ 𝐶 ) ∣ ∀ 𝑖𝑁𝑗𝑁𝑘 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) = ( 0g𝑅 ) } )
6 ssrab2 { 𝑚 ∈ ( Base ‘ 𝐶 ) ∣ ∀ 𝑖𝑁𝑗𝑁𝑘 ∈ ℕ ( ( coe1 ‘ ( 𝑖 𝑚 𝑗 ) ) ‘ 𝑘 ) = ( 0g𝑅 ) } ⊆ ( Base ‘ 𝐶 )
7 5 6 eqsstrdi ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ⊆ ( Base ‘ 𝐶 ) )
8 1 2 3 1elcpmat ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r𝐶 ) ∈ 𝑆 )
9 8 ne0d ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ≠ ∅ )
10 1 2 3 cpmatacl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 ( +g𝐶 ) 𝑦 ) ∈ 𝑆 )
11 1 2 3 cpmatinvcl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑥𝑆 ( ( invg𝐶 ) ‘ 𝑥 ) ∈ 𝑆 )
12 r19.26 ( ∀ 𝑥𝑆 ( ∀ 𝑦𝑆 ( 𝑥 ( +g𝐶 ) 𝑦 ) ∈ 𝑆 ∧ ( ( invg𝐶 ) ‘ 𝑥 ) ∈ 𝑆 ) ↔ ( ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 ( +g𝐶 ) 𝑦 ) ∈ 𝑆 ∧ ∀ 𝑥𝑆 ( ( invg𝐶 ) ‘ 𝑥 ) ∈ 𝑆 ) )
13 10 11 12 sylanbrc ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑥𝑆 ( ∀ 𝑦𝑆 ( 𝑥 ( +g𝐶 ) 𝑦 ) ∈ 𝑆 ∧ ( ( invg𝐶 ) ‘ 𝑥 ) ∈ 𝑆 ) )
14 2 3 pmatring ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ Ring )
15 ringgrp ( 𝐶 ∈ Ring → 𝐶 ∈ Grp )
16 eqid ( +g𝐶 ) = ( +g𝐶 )
17 eqid ( invg𝐶 ) = ( invg𝐶 )
18 4 16 17 issubg2 ( 𝐶 ∈ Grp → ( 𝑆 ∈ ( SubGrp ‘ 𝐶 ) ↔ ( 𝑆 ⊆ ( Base ‘ 𝐶 ) ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥𝑆 ( ∀ 𝑦𝑆 ( 𝑥 ( +g𝐶 ) 𝑦 ) ∈ 𝑆 ∧ ( ( invg𝐶 ) ‘ 𝑥 ) ∈ 𝑆 ) ) ) )
19 14 15 18 3syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑆 ∈ ( SubGrp ‘ 𝐶 ) ↔ ( 𝑆 ⊆ ( Base ‘ 𝐶 ) ∧ 𝑆 ≠ ∅ ∧ ∀ 𝑥𝑆 ( ∀ 𝑦𝑆 ( 𝑥 ( +g𝐶 ) 𝑦 ) ∈ 𝑆 ∧ ( ( invg𝐶 ) ‘ 𝑥 ) ∈ 𝑆 ) ) ) )
20 7 9 13 19 mpbir3and ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ∈ ( SubGrp ‘ 𝐶 ) )