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

Proof

Step Hyp Ref Expression
1 cpmatsrngpmat.s 𝑆 = ( 𝑁 ConstPolyMat 𝑅 )
2 cpmatsrngpmat.p 𝑃 = ( Poly1𝑅 )
3 cpmatsrngpmat.c 𝐶 = ( 𝑁 Mat 𝑃 )
4 1 2 3 cpmatsubgpmat ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ∈ ( SubGrp ‘ 𝐶 ) )
5 1 2 3 1elcpmat ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 1r𝐶 ) ∈ 𝑆 )
6 1 2 3 cpmatmcl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 ( .r𝐶 ) 𝑦 ) ∈ 𝑆 )
7 2 3 pmatring ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝐶 ∈ Ring )
8 eqid ( Base ‘ 𝐶 ) = ( Base ‘ 𝐶 )
9 eqid ( 1r𝐶 ) = ( 1r𝐶 )
10 eqid ( .r𝐶 ) = ( .r𝐶 )
11 8 9 10 issubrg2 ( 𝐶 ∈ Ring → ( 𝑆 ∈ ( SubRing ‘ 𝐶 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝐶 ) ∧ ( 1r𝐶 ) ∈ 𝑆 ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 ( .r𝐶 ) 𝑦 ) ∈ 𝑆 ) ) )
12 7 11 syl ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → ( 𝑆 ∈ ( SubRing ‘ 𝐶 ) ↔ ( 𝑆 ∈ ( SubGrp ‘ 𝐶 ) ∧ ( 1r𝐶 ) ∈ 𝑆 ∧ ∀ 𝑥𝑆𝑦𝑆 ( 𝑥 ( .r𝐶 ) 𝑦 ) ∈ 𝑆 ) ) )
13 4 5 6 12 mpbir3and ( ( 𝑁 ∈ Fin ∧ 𝑅 ∈ Ring ) → 𝑆 ∈ ( SubRing ‘ 𝐶 ) )