proposition: Theorem rank2_char_Sylow_normal gT (G S T : {group gT}) : odd #|G| -> solvable G -> 'r('F(G)) <= 2 -> Sylow G S -> T \char S -> T \subset S^`(1) -> T <| G.
proof: Proof. set F := 'F(G) => oddG solG Fle2 /SylowP[p p_pr sylS] charT sTS'. have [sSG pS _] := and3P sylS. have nsFG: F <| G := Fitting_normal G; have [sFG nFG] := andP nsFG. have nFS := subset_trans sSG nFG; have nilF: nilpotent F := Fitting_nil _. have cGGq: abelian (G / F). by rewrite sub_der1_abelian ?rank2_der1_sub_Fitting. have nsFS_G: F <*> S <| G. rewrite -(quotientGK nsFG) norm_joinEr // -(quotientK nFS) cosetpre_normal. by rewrite -sub_abelian_normal ?quotientS. have sylSF: p.-Sylow(F <*> S) S. by rewrite (pHall_subl _ _ sylS) ?joing_subr // join_subG sFG. have defG: G :=: F * 'N_G(S). rewrite -{1}(Frattini_arg nsFS_G sylSF) /= norm_joinEr // -mulgA. by congr (_ * _); rewrite mulSGid // subsetI sSG normG. rewrite /normal (subset_trans (char_sub charT)) //= defG mulG_subG /= -/F. rewrite setIC andbC subIset /=; last by rewrite (char_norm_trans charT). case/dprodP: (nilpotent_pcoreC p nilF); rewrite /= -/F => _ defF cFpFp' _. have defFp: 'O_p(F) = F :&: S. rewrite -{2}defF -group_modl ?coprime_TIg ?mulg1 //. by rewrite coprime_sym (pnat_coprime pS (pcore_pgroup _ _)). by rewrite p_core_Fitting pcore_sub_Hall. rewrite -defF mulG_subG /= -/F defFp setIC subIset ?(char_norm charT) //=. rewrite cents_norm // (subset_trans cFpFp') // defFp centS // subsetI. rewrite (char_sub charT) (subset_trans (subset_trans sTS' (dergS 1 sSG))) //. exact: rank2_der1_sub_Fitting. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype finfun bigop ssralg finset prime binomial) mathcomp(fingroup morphism automorphism perm quotient action gproduct) mathcomp(gfunctor commutator zmodp cyclic center pgroup gseries nilpotent) mathcomp(sylow abelian maximal extremal hall) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(BGsection1 BGsection2)