Metamath Proof Explorer

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 \in CRing \land M \in B) \to \underset{r \in N}{\sum_{U}} (r M r) \in {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 \in CRing \to U \in CMnd$
7	6	adantr	$⊢ (R \in CRing \land M \in B) \to U \in CMnd$
8	1 2	matrcl	$⊢ M \in B \to (N \in Fin \land R \in V)$
9	8	adantl	$⊢ (R \in CRing \land M \in B) \to (N \in Fin \land R \in V)$
10	9	simpld	$⊢ (R \in CRing \land M \in B) \to N \in Fin$
11		simpr	$⊢ (R \in CRing \land M \in B) \to M \in B$
12	1 4 2	matbas2i	$⊢ M \in B \to M \in ({Base}_{R}^{(N \times N)})$
13		elmapi	$⊢ M \in ({Base}_{R}^{(N \times N)}) \to M : N \times N ⟶ {Base}_{R}$
14	11 12 13	3syl	$⊢ (R \in CRing \land M \in B) \to M : N \times N ⟶ {Base}_{R}$
15	14	adantr	$⊢ ((R \in CRing \land M \in B) \land r \in N) \to M : N \times N ⟶ {Base}_{R}$
16		simpr	$⊢ ((R \in CRing \land M \in B) \land r \in N) \to r \in N$
17	15 16 16	fovcdmd	$⊢ ((R \in CRing \land M \in B) \land r \in N) \to r M r \in {Base}_{R}$
18	17	ralrimiva	$⊢ (R \in CRing \land M \in B) \to \forall r \in N r M r \in {Base}_{R}$
19	5 7 10 18	gsummptcl	$⊢ (R \in CRing \land M \in B) \to \underset{r \in N}{\sum_{U}} (r M r) \in {Base}_{R}$