proposition: Proposition p'core_cent_pgroup gT p (G R : {group gT}) : p.-subgroup(G) R -> solvable G -> 'O_p^'('C_G(R)) \subset 'O_p^'(G).
proof: Proof. case/andP=> sRG pR solG. without loss p'G1: gT G R sRG pR solG / 'O_p^'(G) = 1. have nOG_CR: 'C_G(R) \subset 'N('O_p^'(G)) by rewrite subIset ?gFnorm. move=> IH; rewrite -quotient_sub1 ?gFsub_trans //. apply: subset_trans (morphimF _ _ nOG_CR) _; rewrite /= -quotientE. rewrite -(coprime_subcent_quotient_pgroup pR) ?pcore_sub //; first 1 last. - by rewrite (subset_trans sRG) ?gFnorm. - by rewrite coprime_sym (pnat_coprime _ (pcore_pgroup _ _)). have p'Gq1 : 'O_p^'(G / 'O_p^'(G)) = 1 := trivg_pcore_quotient p^' G. by rewrite -p'Gq1 IH ?morphimS ?morphim_pgroup ?morphim_sol. set M := 'O_p^'('C_G(R)); pose T := 'O_p(G). have /subsetIP[sMG cMR]: M \subset 'C_G(R) by apply: pcore_sub. have [p'M pT]: p^'.-group M /\ p.-group T by rewrite !pcore_pgroup. have nRT: R \subset 'N(T) by rewrite (subset_trans sRG) ?gFnorm. have pRT: p.-group (R <*> T). rewrite -(pquotient_pgroup pT) ?join_subG ?nRT ?normG //=. by rewrite norm_joinEl // quotientMidr morphim_pgroup. have nRT_M: M \subset 'N(R <*> T). by rewrite normsY ?(cents_norm cMR) // (subset_trans sMG) ?gFnorm. have coRT_M: coprime #|R <*> T| #|M| := pnat_coprime pRT p'M. have cMcR: 'C_(R <*> T)(R) \subset 'C(M). apply/commG1P; apply/trivgP; rewrite -(coprime_TIg coRT_M) subsetI commg_subr. rewrite (subset_trans (commSg _ (subsetIl _ _))) ?commg_subl //= -/M. by apply: subset_trans (gFnorm _ _); rewrite setSI // join_subG sRG pcore_sub. have cRT_M: M \subset 'C(R <*> T). rewrite coprime_nil_faithful_cent_stab ?(pgroup_nil pRT) //= -/M. rewrite subsetI subsetIl (subset_trans _ cMcR) // ?setIS ?centS //. by rewrite subsetI joing_subl centsC. have sMT: M \subset T. have defT: 'F(G) = T := Fitting_eq_pcore p'G1. rewrite -defT (subset_trans _ (cent_sub_Fitting solG)) // defT subsetI sMG. by rewrite (subset_trans cRT_M) // centY subsetIr. by rewrite -(setIidPr sMT) p'G1 coprime_TIg // (pnat_coprime pT). 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 gproduct gfunctor commutator) mathcomp(ssralg finalg zmodp cyclic center pgroup finmodule gseries) mathcomp(nilpotent sylow abelian maximal hall extremal) mathcomp(matrix mxalgebra mxrepresentation mxabelem)