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	|- S = ( N ConstPolyMat R )
	cpmatsrngpmat.p	|- P = ( Poly1 ` R )
	cpmatsrngpmat.c	|- C = ( N Mat P )
Assertion	cpmatsubgpmat	|- ( ( N e. Fin /\ R e. Ring ) -> S e. ( SubGrp ` 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		eqid	|- ( Base ` C ) = ( Base ` C )
5	1 2 3 4	cpmat	|- ( ( N e. Fin /\ R e. Ring ) -> S = { m e. ( Base ` C ) | A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` R ) } )
6		ssrab2	|- { m e. ( Base ` C ) | A. i e. N A. j e. N A. k e. NN ( ( coe1 ` ( i m j ) ) ` k ) = ( 0g ` R ) } C_ ( Base ` C )
7	5 6	eqsstrdi	|- ( ( N e. Fin /\ R e. Ring ) -> S C_ ( Base ` C ) )
8	1 2 3	1elcpmat	|- ( ( N e. Fin /\ R e. Ring ) -> ( 1r ` C ) e. S )
9	8	ne0d	|- ( ( N e. Fin /\ R e. Ring ) -> S =/= (/) )
10	1 2 3	cpmatacl	|- ( ( N e. Fin /\ R e. Ring ) -> A. x e. S A. y e. S ( x ( +g ` C ) y ) e. S )
11	1 2 3	cpmatinvcl	|- ( ( N e. Fin /\ R e. Ring ) -> A. x e. S ( ( invg ` C ) ` x ) e. S )
12		r19.26	|- ( A. x e. S ( A. y e. S ( x ( +g ` C ) y ) e. S /\ ( ( invg ` C ) ` x ) e. S ) <-> ( A. x e. S A. y e. S ( x ( +g ` C ) y ) e. S /\ A. x e. S ( ( invg ` C ) ` x ) e. S ) )
13	10 11 12	sylanbrc	|- ( ( N e. Fin /\ R e. Ring ) -> A. x e. S ( A. y e. S ( x ( +g ` C ) y ) e. S /\ ( ( invg ` C ) ` x ) e. S ) )
14	2 3	pmatring	|- ( ( N e. Fin /\ R e. Ring ) -> C e. Ring )
15		ringgrp	|- ( C e. Ring -> C e. Grp )
16		eqid	|- ( +g ` C ) = ( +g ` C )
17		eqid	|- ( invg ` C ) = ( invg ` C )
18	4 16 17	issubg2	|- ( C e. Grp -> ( S e. ( SubGrp ` C ) <-> ( S C_ ( Base ` C ) /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x ( +g ` C ) y ) e. S /\ ( ( invg ` C ) ` x ) e. S ) ) ) )
19	14 15 18	3syl	|- ( ( N e. Fin /\ R e. Ring ) -> ( S e. ( SubGrp ` C ) <-> ( S C_ ( Base ` C ) /\ S =/= (/) /\ A. x e. S ( A. y e. S ( x ( +g ` C ) y ) e. S /\ ( ( invg ` C ) ` x ) e. S ) ) ) )
20	7 9 13 19	mpbir3and	|- ( ( N e. Fin /\ R e. Ring ) -> S e. ( SubGrp ` C ) )