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 ‘ 𝐶 ) )