proposition: Proposition coprime_trivg_cent_Fitting gT (A G : {group gT}) : A \subset 'N(G) -> coprime #|G| #|A| -> solvable G -> 'C_A(G) = 1 -> 'C_A('F(G)) = 1.
proof: Proof. move=> nGA coGA solG regAG; without loss cycA: A nGA coGA regAG / cyclic A. move=> IH; apply/trivgP/subsetP=> a; rewrite -!cycle_subG subsetI. case/andP=> saA /setIidPl <-. rewrite {}IH ?cycle_cyclic ?(coprimegS saA) ?(subset_trans saA) //. by apply/trivgP; rewrite -regAG setSI. pose X := G <*> A; pose F := 'F(X); pose pi := \pi(A); pose Q := 'O_pi(F). have pi'G: pi^'.-group G by rewrite /pgroup -coprime_pi' //= coprime_sym. have piA: pi.-group A by apply: pgroup_pi. have oX: #|X| = (#|G| * #|A|)%N by rewrite [X]norm_joinEr ?coprime_cardMg. have hallG: pi^'.-Hall(X) G. by rewrite /pHall -divgS joing_subl //= pi'G pnatNK oX mulKn. have nsGX: G <| X by rewrite /normal joing_subl join_subG normG. have{oX pi'G piA} hallA: pi.-Hall(X) A. by rewrite /pHall -divgS joing_subr //= piA oX mulnK. have nsQX: Q <| X by rewrite !gFnormal_trans. have{solG cycA} solX: solvable X. rewrite (series_sol nsGX) {}solG /= norm_joinEr // quotientMidl //. by rewrite morphim_sol // abelian_sol // cyclic_abelian. have sQA: Q \subset A. by apply: normal_sub_max_pgroup (Hall_max hallA) (pcore_pgroup _ _) nsQX. have pi'F: 'O_pi(F) = 1. suff cQG: G \subset 'C(Q) by apply/trivgP; rewrite -regAG subsetI sQA centsC. apply/commG1P/trivgP; rewrite -(coprime_TIg coGA) subsetI commg_subl. rewrite (subset_trans sQA) // (subset_trans _ sQA) // commg_subr. by rewrite (subset_trans _ (normal_norm nsQX)) ?joing_subl. have sFG: F \subset G. have /dprodP[_ defF _ _]: _ = F := nilpotent_pcoreC pi (Fitting_nil _). by rewrite (sub_normal_Hall hallG) ?gFsub //= -defF pi'F mul1g pcore_pgroup. have <-: F = 'F(G). apply/eqP; rewrite eqEsubset -{1}(setIidPr sFG) FittingS ?joing_subl //=. by rewrite Fitting_max ?Fitting_nil // gFnormal_trans. apply/trivgP; rewrite /= -(coprime_TIg coGA) subsetI subsetIl andbT. apply: subset_trans (subset_trans (cent_sub_Fitting solX) sFG). by rewrite setSI ?joing_subr. 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)