Theorem matgsumcl

Description: Closure of a group sum over the diagonal coefficients of a square matrix over a commutative ring. (Contributed by AV, 29-Dec-2018) (Proof shortened by AV, 23-Jul-2019)

	Ref	Expression
Hypotheses	madetsumid.a	|- A = ( N Mat R )
	madetsumid.b	|- B = ( Base ` A )
	madetsumid.u	|- U = ( mulGrp ` R )
Assertion	matgsumcl	|- ( ( R e. CRing /\ M e. B ) -> ( U gsum ( r e. N |-> ( r M r ) ) ) e. ( Base ` R ) )

Proof

Step	Hyp	Ref	Expression
1		madetsumid.a	|- A = ( N Mat R )
2		madetsumid.b	|- B = ( Base ` A )
3		madetsumid.u	|- U = ( mulGrp ` R )
4		eqid	|- ( Base ` R ) = ( Base ` R )
5	3 4	mgpbas	|- ( Base ` R ) = ( Base ` U )
6	3	crngmgp	|- ( R e. CRing -> U e. CMnd )
7	6	adantr	|- ( ( R e. CRing /\ M e. B ) -> U e. CMnd )
8	1 2	matrcl	|- ( M e. B -> ( N e. Fin /\ R e. _V ) )
9	8	adantl	|- ( ( R e. CRing /\ M e. B ) -> ( N e. Fin /\ R e. _V ) )
10	9	simpld	|- ( ( R e. CRing /\ M e. B ) -> N e. Fin )
11		simpr	|- ( ( R e. CRing /\ M e. B ) -> M e. B )
12	1 4 2	matbas2i	|- ( M e. B -> M e. ( ( Base ` R ) ^m ( N X. N ) ) )
13		elmapi	|- ( M e. ( ( Base ` R ) ^m ( N X. N ) ) -> M : ( N X. N ) --> ( Base ` R ) )
14	11 12 13	3syl	|- ( ( R e. CRing /\ M e. B ) -> M : ( N X. N ) --> ( Base ` R ) )
15	14	adantr	|- ( ( ( R e. CRing /\ M e. B ) /\ r e. N ) -> M : ( N X. N ) --> ( Base ` R ) )
16		simpr	|- ( ( ( R e. CRing /\ M e. B ) /\ r e. N ) -> r e. N )
17	15 16 16	fovrnd	|- ( ( ( R e. CRing /\ M e. B ) /\ r e. N ) -> ( r M r ) e. ( Base ` R ) )
18	17	ralrimiva	|- ( ( R e. CRing /\ M e. B ) -> A. r e. N ( r M r ) e. ( Base ` R ) )
19	5 7 10 18	gsummptcl	|- ( ( R e. CRing /\ M e. B ) -> ( U gsum ( r e. N |-> ( r M r ) ) ) e. ( Base ` R ) )