proposition: Theorem rank2_der1_complement gT p (G : {group gT}) : solvable G -> odd #|G| -> 'r_p(G) <= 2 -> [/\ p^'.-Hall(G^`(1)) 'O_p^'(G^`(1)), abelian (G / 'O_{p^',p}(G)) & p^'.-group (G / 'O_{p^',p}(G))].
proof: Proof. move=> solG oddG rG; rewrite /pHall pcore_sub pcore_pgroup /= pnatNK. rewrite -(pcore_setI_normal _ (der_normal 1 G)) // setIC indexgI /=. without loss Gp'1: gT G solG oddG rG / 'O_p^'(G) = 1. have nsGp': 'O_p^'(G) <| G := pcore_normal p^' G; have [_ nGp'] := andP nsGp'. move/(_ _ (G / 'O_p^'(G))%G); rewrite quotient_sol // quotient_odd //=. have Gp'1 := trivg_pcore_quotient p^' G. rewrite p_rank_p'quotient ?pcore_pgroup // Gp'1 indexg1 => -[] //=. rewrite -quotient_der // card_quotient ?gFsub_trans // => ->. rewrite (pseries_pop2 _ Gp'1) /= -pseries1 -quotient_pseries /= /pgroup. pose isos := (isog_abelian (third_isog _ _ _), card_isog (third_isog _ _ _)). by rewrite !{}isos ?pseries_normal ?pseries_sub_catl. rewrite pseries_pop2 // Gp'1 indexg1 -pgroupE /=. set R := 'O_p(G); pose C := 'C_G(R). have /andP[sRG nRG]: R <| G by apply: gFnormal. have sCR: C \subset R by rewrite /C /R -(Fitting_eq_pcore _) ?cent_sub_Fitting. have pR: p.-group R := pcore_pgroup p G; have pC: p.-group C := pgroupS sCR pR. have nCG: G \subset 'N(C) by rewrite normsI ?normG ?norms_cent. have nsG'G: G^`(1) <| G := der_normal 1 G; have [sG'G nG'G] := andP nsG'G. suffices sG'R: G^`(1) \subset R. have cGbGb: abelian (G / R) := sub_der1_abelian sG'R. rewrite -{2}(nilpotent_pcoreC p (abelian_nil cGbGb)) trivg_pcore_quotient. by rewrite dprod1g pcore_pgroup (pgroupS sG'R pR). rewrite pcore_max // -(pquotient_pgroup pC (subset_trans sG'G nCG)) /= -/C. pose A := conj_aut 'O_p(G) @* G; have AutA: A \subset Aut R := Aut_conj_aut _ G. have isoGbA: G / C \isog A by rewrite /C -ker_conj_aut first_isog_loc. have{isoGbA} [f injf defA] := isogP isoGbA; rewrite /= -/A in defA. rewrite quotient_der // /pgroup -(card_injm injf) ?der_sub ?morphim_der //. have [? ?]: odd #|A| /\ solvable A by rewrite -defA !morphim_odd ?morphim_sol. have rR: 'r(R) <= 2 by rewrite (rank_pgroup pR) (leq_trans (p_rankS p sRG)). by rewrite defA -pgroupE (der1_Aut_rank2_pgroup pR) ?(oddSg sRG). 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)