proposition: Proposition mxdirect_sum_proj_eigenspace_cycle : (sumE :=: 1%:M)%MS /\ mxdirect sumE.
proof: Proof. have [def1V] := mxdirect_sum_eigenspace_cycle; move/mxdirect_sumsP=> dxV. pose p (i : 'I_h) := proj_mx 'V_i (\sum_(j | j != i) 'V_j)%MS. have def1p: 1%:M = \sum_i p i. rewrite -[\sum_i _]mul1mx; move/eqmxP: def1V; rewrite submx1. case/sub_sumsmxP=> u ->; rewrite mulmx_sumr; apply: eq_bigr => i _. rewrite (bigD1 i) //= mulmxDl proj_mx_id ?submxMl ?dxV //. rewrite proj_mx_0 ?dxV ?addr0 ?summx_sub // => j ne_ji. by rewrite (sumsmx_sup j) ?submxMl. split; first do [apply/eqmxP; rewrite submx1]. apply/(@memmx_subP F _ _ q)=> A _; apply/memmx_sumsP. pose B i t := p i *m A *m p t. exists (fun it => B it.1 it.2) => [|[i t] /=]. rewrite -(pair_bigA _ B) /= -[A]mul1mx def1p mulmx_suml. by apply: eq_bigr => i _; rewrite -mulmx_sumr -def1p mulmx1. apply/E2iP; split=> [|j ne_ji]; first by rewrite mulmxA proj_mx_sub. rewrite 2!mulmxA -mulmxA proj_mx_0 ?dxV ?mul0mx //. rewrite (sumsmx_sup (inh j)) ?Vi_mod //. by rewrite (modn_small (valP i)) in ne_ji. apply/mxdirect_sumsP=> [[i t] _] /=. apply/eqP; rewrite -submx0; apply/(@memmx_subP F _ _ q)=> A. rewrite sub_capmx submx0 mxvec_eq0 -submx0. case/andP=> /E2iP[ViA Vi'A] /memmx_sumsP[B /= defA sBE]. rewrite -[A]mul1mx -(eqmxMr A def1V) sumsmxMr (bigD1 i) //=. rewrite big1 ?addsmx0 => [|j ne_ij]; last by rewrite Vi'A ?modn_small. rewrite -[_ *m A]mulmx1 def1p mulmx_sumr (bigD1 t) //=. rewrite big1 ?addr0 => [|u ne_ut]; last first. by rewrite proj_mx_0 ?dxV ?(sumsmx_sup t) // eq_sym. rewrite {A ViA Vi'A}defA mulmx_sumr mulmx_suml summx_sub // => [[j u]]. case/E2iP: (sBE (j, u)); rewrite eqE /=; case: eqP => [-> sBu _ ne_ut|]. by rewrite proj_mx_0 ?dxV ?(sumsmx_sup u). by move/eqP=> ne_ji _ ->; rewrite ?mul0mx // eq_sym !modn_small. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div fintype) mathcomp(bigop prime binomial finset fingroup morphism perm automorphism) mathcomp(quotient action gfunctor commutator gproduct) mathcomp(ssralg finalg zmodp cyclic center pgroup gseries nilpotent) mathcomp(sylow abelian maximal hall) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(BGsection1)