proposition: Lemma mxtrace_dsum_mod (I : finType) (P : pred I) U W (modU : forall i, mG (U i)) (modW : mG W) : let S := (\sum_(i | P i) U i)%MS in (S :=: W)%MS -> mxdirect S -> {in G, forall x, \sum_(i | P i) \tr (sr (modU i) x) = \tr (sr modW x)}.
proof: Proof. move=> /= sumS dxS x Gx; have [m lePm] := ubnP #|P|. elim: m => // m IHm in P lePm W modW sumS dxS *. have [j /= Pj | P0] := pickP P; last first. case: sumS (_ x); rewrite !big_pred0 // mxrank0 => <- _ rWx. by rewrite [rWx]flatmx0 linear0. rewrite ltnS (cardD1x Pj) in lePm. rewrite mxdirectE /= !(bigD1 j Pj) -mxdirectE mxdirect_addsE /= in dxS sumS *. have [_ dxW' dxW] := and3P dxS; rewrite (sameP eqP mxdirect_addsP) in dxW. rewrite (IHm _ _ _ (sumsmx_module _ (fun i _ => modU i)) (eqmx_refl _)) //. exact: mxtrace_dadd_mod. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly polydiv finset fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup matrix mxalgebra) mathcomp(mxpoly)