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	|- S = ( N ConstPolyMat R )
	cpmatsrngpmat.p	|- P = ( Poly1 ` R )
	cpmatsrngpmat.c	|- C = ( N Mat P )
Assertion	cpmatsrgpmat	|- ( ( N e. Fin /\ R e. Ring ) -> S e. ( SubRing ` C ) )

Proof

Step	Hyp	Ref	Expression
1		cpmatsrngpmat.s	|- S = ( N ConstPolyMat R )
2		cpmatsrngpmat.p	|- P = ( Poly1 ` R )
3		cpmatsrngpmat.c	|- C = ( N Mat P )
4	1 2 3	cpmatsubgpmat	|- ( ( N e. Fin /\ R e. Ring ) -> S e. ( SubGrp ` C ) )
5	1 2 3	1elcpmat	|- ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` C ) e. S )
6	1 2 3	cpmatmcl	|- ( ( N e. Fin /\ R e. Ring ) -> A. x e. S A. y e. S ( x ( .r ` C ) y ) e. S )
7	2 3	pmatring	|- ( ( N e. Fin /\ R e. Ring ) -> C e. Ring )
8		eqid	|- ( Base ` C ) = ( Base ` C )
9		eqid	|- ( 1r ` C ) = ( 1r ` C )
10		eqid	|- ( .r ` C ) = ( .r ` C )
11	8 9 10	issubrg2	|- ( C e. Ring -> ( S e. ( SubRing ` C ) <-> ( S e. ( SubGrp ` C ) /\ ( 1r ` C ) e. S /\ A. x e. S A. y e. S ( x ( .r ` C ) y ) e. S ) ) )
12	7 11	syl	|- ( ( N e. Fin /\ R e. Ring ) -> ( S e. ( SubRing ` C ) <-> ( S e. ( SubGrp ` C ) /\ ( 1r ` C ) e. S /\ A. x e. S A. y e. S ( x ( .r ` C ) y ) e. S ) ) )
13	4 5 6 12	mpbir3and	|- ( ( N e. Fin /\ R e. Ring ) -> S e. ( SubRing ` C ) )