proposition: Theorem narrow_der1_complement_max_pdiv gT p (G S : {group gT}) : odd #|G| -> solvable G -> p.-Sylow(G) S -> p.-narrow S -> (2 < 'r(S)) ==> p.-length_1 G -> [/\ p^'.-Hall(G^`(1)) 'O_p^'(G^`(1)) & forall q, q \in \pi(G / 'O_p^'(G)) -> q <= p].
proof: Proof. move=> oddG solG sylS nnS; case: (leqP 'r(S) 2) => /= rS pl1G. have rG: 'r_p(G) <= 2 by rewrite -(rank_Sylow sylS). split=> [|q]; first by have [-> _ _] := rank2_der1_complement solG oddG rG. exact: rank2_max_pdiv solG oddG rG. rewrite /pHall pcore_sub pcore_pgroup pnatNK /=. rewrite -(pcore_setI_normal p^' (der_normal 1 G)) // setIC indexgI /=. wlog Gp'1: gT G S oddG nnS solG sylS rS pl1G / 'O_p^'(G) = 1. set K := 'O_p^'(G); have [_ nKG] := andP (pcore_normal _ G : K <| G). move/(_ _ (G / K) (S / K))%G; rewrite quotient_sol ?quotient_odd //. have [[sSG pS _] p'K] := (and3P sylS, pcore_pgroup _ G : p^'.-group K). have [nKS nKG'] := (subset_trans sSG nKG, subset_trans (der_sub 1 G) nKG). have tiKS: K :&: S = 1 := coprime_TIg (p'nat_coprime p'K pS). have isoS := isog_symr (quotient_isog nKS tiKS). rewrite (isog_narrow p isoS) {isoS}(isog_rank isoS) quotient_pHall //. rewrite plength1_quo // trivg_pcore_quotient indexg1 /= -quotient_der //. by rewrite card_quotient //= -/K -(card_isog (quotient1_isog _)); apply. rewrite Gp'1 indexg1 -(card_isog (quotient1_isog _)) -pgroupE. have [sSG pS _] := and3P sylS; have oddS: odd #|S| := oddSg sSG oddG. have ntS: S :!=: 1 by rewrite -rank_gt0 (leq_trans _ rS). have [p_pr _ _] := pgroup_pdiv pS ntS; have p_gt1 := prime_gt1 p_pr. have{pl1G} defS: 'O_p(G) = S. by rewrite (eq_Hall_pcore _ sylS) -?plength1_pcore_Sylow. have nSG: G \subset 'N(S) by rewrite -defS gFnorm. pose fA := restrm nSG (conj_aut S); pose A := fA @* G. have AutA: A \subset Aut S by rewrite [A]im_restrm Aut_conj_aut. have [solA oddA]: solvable A /\ odd #|A| by rewrite morphim_sol ?morphim_odd. have [/= _ cAbAb p'A_dv_p1] := Aut_narrow pS oddS nnS solA AutA oddA. have{defS} pKfA: p.-group ('ker fA). rewrite (pgroupS _ pS) //= ker_restrm ker_conj_aut. by rewrite -defS -Fitting_eq_pcore ?cent_sub_Fitting. split=> [|q]. rewrite -(pmorphim_pgroup pKfA) ?der_sub // morphim_der //. by rewrite (pgroupS (der1_min _ cAbAb)) ?pcore_pgroup ?gFnorm. rewrite mem_primes => /and3P[q_pr _ /Cauchy[] // x Gx ox]. rewrite leq_eqVlt -implyNb; apply/implyP=> p'q; rewrite -(ltn_predK p_gt1) ltnS. have ofAx: #[fA x] = q. apply/prime_nt_dvdP=> //; last by rewrite -ox morph_order. rewrite order_eq1; apply: contraNneq p'q => fAx1. by apply: (pgroupP pKfA); rewrite // -ox order_dvdG //; apply/kerP. have p'fAx: p^'.-elt (fA x) by rewrite /p_elt ofAx pnatE. by rewrite -ofAx dvdn_leq ?p'A_dv_p1 ?mem_morphim // -(subnKC p_gt1). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype finset prime fingroup morphism perm automorphism action) mathcomp(quotient cyclic gfunctor pgroup gproduct center commutator) mathcomp(gseries nilpotent sylow abelian maximal hall) odd_order(BGsection1 BGsection4)