This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝐴 = ( 𝑁 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 fovcdmd ⊢ ( ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) ∧ 𝑟 ∈ 𝑁 ) → ( 𝑟 𝑀 𝑟 ) ∈ ( Base ‘ 𝑅 ) )
18 17 ralrimiva ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ∀ 𝑟 ∈ 𝑁 ( 𝑟 𝑀 𝑟 ) ∈ ( Base ‘ 𝑅 ) )
19 5 7 10 18 gsummptcl ⊢ ( ( 𝑅 ∈ CRing ∧ 𝑀 ∈ 𝐵 ) → ( 𝑈 Σg ( 𝑟 ∈ 𝑁 ↦ ( 𝑟 𝑀 𝑟 ) ) ) ∈ ( Base ‘ 𝑅 ) )