proposition: Lemma mxdirect_sums_center (I : finType) m n (R : 'A_(m, n)) R_ : (\sum_i R_ i :=: R)%MS -> mxdirect (\sum_i R_ i) -> (forall i : I, mx_ideal R (R_ i)) -> ('Z(R) :=: \sum_i 'Z(R_ i))%MS.
proof: Proof. move=> defR dxR idealR. have sR_R: (R_ _ <= R)%MS by move=> i; rewrite -defR (sumsmx_sup i). have anhR i j A B : i != j -> A \in R_ i -> B \in R_ j -> A *m B = 0. move=> ne_ij RiA RjB; apply: memmx0. have [[_ idRiR] [idRRj _]] := (andP (idealR i), andP (idealR j)). rewrite -(mxdirect_sumsP dxR j) // sub_capmx (sumsmx_sup i) //. by rewrite (mulsmx_subP idRRj) // (memmx_subP (sR_R i)). by rewrite (mulsmx_subP idRiR) // (memmx_subP (sR_R j)). apply/eqmxP/andP; split. apply/memmx_subP=> Z; rewrite sub_capmx => /andP[]. rewrite -{1}defR => /memmx_sumsP[z ->{Z} Rz cRz]. apply/memmx_sumsP; exists z => // i; rewrite sub_capmx Rz. apply/cent_mxP=> A RiA; have:= cent_mxP cRz A (memmx_subP (sR_R i) A RiA). rewrite (bigD1 i) //= mulmxDl mulmxDr mulmx_suml mulmx_sumr. by rewrite !big1 ?addr0 // => j; last rewrite eq_sym; move/anhR->. apply/sumsmx_subP => i _; apply/memmx_subP=> z; rewrite sub_capmx. case/andP=> Riz cRiz; rewrite sub_capmx (memmx_subP (sR_R i)) //=. apply/cent_mxP=> A; rewrite -{1}defR; case/memmx_sumsP=> a -> R_a. rewrite (bigD1 i) // mulmxDl mulmxDr mulmx_suml mulmx_sumr. rewrite !big1 => [|j|j]; first by rewrite !addr0 (cent_mxP cRiz). by rewrite eq_sym => /anhR->. by move/anhR->. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(fintype finfun bigop finset fingroup perm order) mathcomp(div prime binomial ssralg finalg zmodp matrix)