proposition: Lemma mxdirect_sum_eigenspace (P : pred I) a_ : {in P &, injective a_} -> mxdirect (\sum_(i | P i) eigenspace (a_ i)).
proof: Proof. have [m] := ubnP #|P|; elim: m P => // m IHm P lePm inj_a. apply/mxdirect_sumsP=> i Pi; apply/eqP/rowV0P => v. rewrite sub_capmx => /andP[/eigenspaceP def_vg]. set Vi' := (\sum_(i | _) _)%MS => Vi'v. have dxVi': mxdirect Vi'. rewrite (cardD1x Pi) in lePm; apply: IHm => //. by apply: sub_in2 inj_a => j /andP[]. case/sub_dsumsmx: Vi'v => // u Vi'u def_v _. rewrite def_v big1 // => j Pi'j; apply/eqP. have nz_aij: a_ i - a_ j != 0. by case/andP: Pi'j => Pj ne_ji; rewrite subr_eq0 eq_sym (inj_in_eq inj_a). case: (sub_dsumsmx dxVi' (sub0mx 1 _)) => C _ _ uniqC. rewrite -(eqmx_eq0 (eqmx_scale _ nz_aij)). rewrite (uniqC (fun k => (a_ i - a_ k) *: u k)) => // [|k Pi'k|]. - by rewrite -(uniqC (fun _ => 0)) ?big1 // => k Pi'k; apply: sub0mx. - by rewrite scalemx_sub ?Vi'u. rewrite -{1}(subrr (v *m g)) {1}def_vg def_v scaler_sumr mulmx_suml -sumrB. by apply: eq_bigr => k /Vi'u/eigenspaceP->; rewrite scalerBl. 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)