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	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
	madetsumid.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
	madetsumid.u	⊢ 𝑈 = ( mulGrp ‘ 𝑅 )
Assertion	matgsumcl	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑀 𝑟 ) ) ) ∈ ( Base ‘ 𝑅 ) )

Proof

Step	Hyp	Ref	Expression
1		madetsumid.a	⊢ 𝐴 = ( 𝑁 Mat 𝑅 )
2		madetsumid.b	⊢ 𝐵 = ( Base ‘ 𝐴 )
3		madetsumid.u	⊢ 𝑈 = ( mulGrp ‘ 𝑅 )
4		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
5	3 4	mgpbas	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑈 )
6	3	crngmgp	⊢ ( 𝑅 ∈ CRing → 𝑈 ∈ CMnd )
7	6	adantr	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑈 ∈ CMnd )
8	1 2	matrcl	⊢ ( 𝑀 ∈ 𝐵 → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
9	8	adantl	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑁 ∈ Fin ∧ 𝑅 ∈ V ) )
10	9	simpld	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑁 ∈ Fin )
11		simpr	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑀 ∈ 𝐵 )
12	1 4 2	matbas2i	⊢ ( 𝑀 ∈ 𝐵 → 𝑀 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) )
13		elmapi	⊢ ( 𝑀 ∈ ( ( Base ‘ 𝑅 ) ↑m ( 𝑁 × 𝑁 ) ) → 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
14	11 12 13	3syl	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
15	14	adantr	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝑁 ) → 𝑀 : ( 𝑁 × 𝑁 ) ⟶ ( Base ‘ 𝑅 ) )
16		simpr	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝑁 ) → 𝑟 ∈ 𝑁 )
17	15 16 16	fovrnd	⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝑁 ) → ( 𝑟 𝑀 𝑟 ) ∈ ( Base ‘ 𝑅 ) )
18	17	ralrimiva	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∀ 𝑟 ∈ 𝑁 ( 𝑟 𝑀 𝑟 ) ∈ ( Base ‘ 𝑅 ) )
19	5 7 10 18	gsummptcl	⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑀 𝑟 ) ) ) ∈ ( Base ‘ 𝑅 ) )