proposition: Lemma mxdirect_adds_center m1 m2 n (R1 : 'A_(m1, n)) (R2 : 'A_(m2, n)) : mx_ideal (R1 + R2)%MS R1 -> mx_ideal (R1 + R2)%MS R2 -> mxdirect (R1 + R2) -> ('Z((R1 + R2)%MS) :=: 'Z(R1) + 'Z(R2))%MS.
proof: Proof. case/andP=> idlR1 idrR1 /andP[idlR2 idrR2] /mxdirect_addsP dxR12. apply/eqmxP/andP; split. apply/memmx_subP=> z0; rewrite sub_capmx => /andP[]. case/memmx_addsP=> z [R1z1 R2z2 ->{z0}] Cz. rewrite linearD addmx_sub_adds //= ?sub_capmx ?R1z1 ?R2z2 /=. apply/cent_mxP=> A R1_A; have R_A := submx_trans R1_A (addsmxSl R1 R2). have Rz2 := submx_trans R2z2 (addsmxSr R1 R2). rewrite -{1}[z.1](addrK z.2) mulmxBr (cent_mxP Cz) // mulmxDl. rewrite [A *m z.2]memmx0 1?[z.2 *m A]memmx0 ?addrK //. by rewrite -dxR12 sub_capmx (mulsmx_subP idlR1) // (mulsmx_subP idrR2). by rewrite -dxR12 sub_capmx (mulsmx_subP idrR1) // (mulsmx_subP idlR2). apply/cent_mxP=> A R2_A; have R_A := submx_trans R2_A (addsmxSr R1 R2). have Rz1 := submx_trans R1z1 (addsmxSl R1 R2). rewrite -{1}[z.2](addKr z.1) mulmxDr (cent_mxP Cz) // mulmxDl. rewrite mulmxN [A *m z.1]memmx0 1?[z.1 *m A]memmx0 ?addKr //. by rewrite -dxR12 sub_capmx (mulsmx_subP idrR1) // (mulsmx_subP idlR2). by rewrite -dxR12 sub_capmx (mulsmx_subP idlR1) // (mulsmx_subP idrR2). rewrite addsmx_sub; apply/andP; split. apply/memmx_subP=> z; rewrite sub_capmx => /andP[R1z cR1z]. have Rz := submx_trans R1z (addsmxSl R1 R2). rewrite sub_capmx Rz; apply/cent_mxP=> A0. case/memmx_addsP=> A [R1_A1 R2_A2] ->{A0}. have R_A2 := submx_trans R2_A2 (addsmxSr R1 R2). rewrite mulmxDl mulmxDr (cent_mxP cR1z) //; congr (_ + _). rewrite [A.2 *m z]memmx0 1?[z *m A.2]memmx0 //. by rewrite -dxR12 sub_capmx (mulsmx_subP idrR1) // (mulsmx_subP idlR2). by rewrite -dxR12 sub_capmx (mulsmx_subP idlR1) // (mulsmx_subP idrR2). apply/memmx_subP=> z; rewrite !sub_capmx => /andP[R2z cR2z]. have Rz := submx_trans R2z (addsmxSr R1 R2); rewrite Rz. apply/cent_mxP=> _ /memmx_addsP[A [R1_A1 R2_A2 ->]]. rewrite mulmxDl mulmxDr (cent_mxP cR2z _ R2_A2) //; congr (_ + _). have R_A1 := submx_trans R1_A1 (addsmxSl R1 R2). rewrite [A.1 *m z]memmx0 1?[z *m A.1]memmx0 //. by rewrite -dxR12 sub_capmx (mulsmx_subP idlR1) // (mulsmx_subP idrR2). by rewrite -dxR12 sub_capmx (mulsmx_subP idrR1) // (mulsmx_subP idlR2). 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)