proposition: Lemma Clifford_basis M : mxsimple rH M -> {X : {set gT} | X \subset G & let S := \sum_(x in X) M *m rG x in S :=: 1%:M /\ mxdirect S}%MS.
proof: Proof. move=> simM. have simMG (g : [subg G]) : mxsimple rH (M *m rG (val g)). by case: g => x Gx; apply: Clifford_simple. have [|XG [defX1 dxX1]] := sum_mxsimple_direct_sub simMG (_ : _ :=: 1%:M)%MS. apply/eqmxP; case irrG => _ _ ->; rewrite ?submx1 //; last first. rewrite -submx0; apply/sumsmx_subP; move/(_ 1%g (erefl _)); apply: negP. by rewrite submx0 repr_mx1 mulmx1; case simM. apply/mxmoduleP=> x Gx; rewrite sumsmxMr; apply/sumsmx_subP=> [[y Gy]] /= _. by rewrite (sumsmx_sup (subg G (y * x)))// subgK ?groupM// -mulmxA repr_mxM. exists (val @: XG); first by apply/subsetP=> ?; case/imsetP=> [[x Gx]] _ ->. have bij_val: {on val @: XG, bijective (@sgval _ G)}. exists (subg G) => [g _ | x]; first exact: sgvalK. by case/imsetP=> [[x' Gx]] _ ->; rewrite subgK. have defXG g: (val g \in val @: XG) = (g \in XG). by apply/imsetP/idP=> [[h XGh] | XGg]; [move/val_inj-> | exists g]. by rewrite /= mxdirectE /= !(reindex _ bij_val) !(eq_bigl _ _ defXG). 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)