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 ⊢ A = N Mat R
madetsumid.b ⊢ B = Base A
madetsumid.u ⊢ U = mulGrp R
Assertion matgsumcl ⊢ R ∈ CRing ∧ M ∈ B → ∑ U r ∈ N r M r ∈ 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 ∈ CRing → U ∈ CMnd
7 6 adantr ⊢ R ∈ CRing ∧ M ∈ B → U ∈ CMnd
8 1 2 matrcl ⊢ M ∈ B → N ∈ Fin ∧ R ∈ V
9 8 adantl ⊢ R ∈ CRing ∧ M ∈ B → N ∈ Fin ∧ R ∈ V
10 9 simpld ⊢ R ∈ CRing ∧ M ∈ B → N ∈ Fin
11 simpr ⊢ R ∈ CRing ∧ M ∈ B → M ∈ B
12 1 4 2 matbas2i ⊢ M ∈ B → M ∈ Base R N × N
13 elmapi ⊢ M ∈ Base R N × N → M : N × N ⟶ Base R
14 11 12 13 3syl ⊢ R ∈ CRing ∧ M ∈ B → M : N × N ⟶ Base R
15 14 adantr ⊢ R ∈ CRing ∧ M ∈ B ∧ r ∈ N → M : N × N ⟶ Base R
16 simpr ⊢ R ∈ CRing ∧ M ∈ B ∧ r ∈ N → r ∈ N
17 15 16 16 fovcdmd ⊢ R ∈ CRing ∧ M ∈ B ∧ r ∈ N → r M r ∈ Base R
18 17 ralrimiva ⊢ R ∈ CRing ∧ M ∈ B → ∀ r ∈ N r M r ∈ Base R
19 5 7 10 18 gsummptcl ⊢ R ∈ CRing ∧ M ∈ B → ∑ U r ∈ N r M r ∈ Base R