proposition: Lemma pcore_sub_rstab_mxsimple M : mxsimple rG M -> 'O_p(G) \subset rstab rG M.
proof: Proof. case=> modM nzM simM; have sGpG := pcore_sub p G. rewrite rfix_mx_rstabC //; set U := rfix_mx _ _. have:= simM (M :&: U)%MS; rewrite sub_capmx submx_refl. apply; rewrite ?capmxSl //. by rewrite capmx_module // normal_rfix_mx_module ?pcore_normal. rewrite -(in_submodK (capmxSl _ _)) val_submod_eq0 -submx0. rewrite -(rfix_submod modM) // submx0 rfix_pgroup_char ?pcore_pgroup //. by rewrite lt0n mxrank_eq0. 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)