proposition: Lemma mxsimple_abelemP (U : 'M['F_p]_n) : reflect (mxsimple rG U) (minnormal (rV_E @* rowg U) G).
proof: Proof. apply: (iffP mingroupP) => [[/andP[ntU modU] minU] | [modU ntU minU]]. split=> [||V modV sVU ntV]; first by rewrite mxmodule_abelem. by apply: contraNneq ntU => ->; rewrite /= rowg0 morphim1. rewrite -rowgS -rVabelemS [_ @* rowg V]minU //. rewrite -subG1 sub_rVabelem_im morphim1 subG1 trivg_rowg ntV /=. by rewrite -mxmodule_abelem. by rewrite rVabelemS rowgS. split=> [|D /andP[ntD nDG sDU]]. rewrite -subG1 sub_rVabelem_im morphim1 subG1 trivg_rowg ntU /=. by rewrite -mxmodule_abelem. apply/eqP; rewrite eqEsubset sDU sub_rVabelem_im /= -rowg_mxSK rowgK. have sDE: D \subset E := subset_trans sDU (sub_rVabelem _). rewrite minU ?mxmodule_abelemG //. by rewrite -rowgS rowg_mxK sub_abelem_rV_im. by rewrite rowg_mx_eq0 (morphim_injm_eq1 abelem_rV_injm). Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly finset fingroup morphism perm) mathcomp(automorphism quotient gproduct action finalg) mathcomp(zmodp commutator cyclic center pgroup gseries) mathcomp(nilpotent sylow maximal abelian matrix) mathcomp(mxalgebra mxrepresentation)