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