proposition: Lemma mxtrace_dadd_mod U V W (modU : mG U) (modV : mG V) (modW : mG W) : (U + V :=: W)%MS -> mxdirect (U + V) -> {in G, forall x, \tr (sr modU x) + \tr (sr modV x) = \tr (sr modW x)}.
proof: Proof. move=> defW dxW x Gx; have [sUW sVW]: (U <= W)%MS /\ (V <= W)%MS. by apply/andP; rewrite -addsmx_sub defW. pose U' := <<in_submod W U>>%MS; pose V' := <<in_submod W V>>%MS. have addUV': (U' + V' :=: 1%:M)%MS. apply/eqmxP; rewrite submx1 /= (adds_eqmx (genmxE _) (genmxE _)). by rewrite -addsmxMr -val_submodS val_submod1 in_submodK ?defW. have dxUV': mxdirect (U' + V'). apply/eqnP; rewrite /= addUV' mxrank1 !genmxE !mxrank_in_submod //. by rewrite -(mxdirectP dxW) /= defW. have [modU' simU] := mx_rsim_in_submod modU modW sUW. have [modV' simV] := mx_rsim_in_submod modV modW sVW. rewrite (mxtrace_rsim simU) // (mxtrace_rsim simV) //. rewrite -(mxtrace_sub_fact_mod modV') addrC; congr (_ + _). by rewrite (mxtrace_rsim (mx_rsim_factmod modU' modV' addUV' dxUV')). 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)