proposition: Lemma sigma_compl_context M E E1 E2 E3 : M \in 'M -> sigma_complement M E E1 E2 E3 -> [/\ E3 \subset E^`(1) /\ E3 <| E, E2 :==: 1 -> E1 :!=: 1, cyclic E1 /\ cyclic E3, E3 ><| (E2 ><| E1) = E /\ E3 ><| E2 ><| E1 = E & 'C_E3(E) = 1].
proof: Proof. move=> maxM [hallE hallE1 hallE2 hallE3 groupE21]. have [sEM solM] := (pHall_sub hallE, mmax_sol maxM). have [[sE1E t1E1 _] [sE3E t3E3 _]] := (and3P hallE1, and3P hallE3). have tiE'E1: E^`(1) :&: E1 = 1. rewrite coprime_TIg // coprime_pi' ?cardG_gt0 //. by apply: sub_pgroup t1E1 => p; rewrite (tau1E maxM hallE) => /and3P[]. have cycE1: cyclic E1. apply: nil_Zgroup_cyclic. rewrite odd_rank1_Zgroup ?mFT_odd //; apply: wlog_neg; rewrite -ltnNge. have [p p_pr ->]:= rank_witness E1; move/ltnW; rewrite p_rank_gt0. move/(pnatPpi t1E1); rewrite (tau1E maxM hallE) => /and3P[_ _ /eqP <-]. by rewrite p_rankS. rewrite abelian_nil // /abelian (sameP commG1P trivgP) -tiE'E1. by rewrite subsetI (der_sub 1) (dergS 1). have solE: solvable E := solvableS sEM solM. have nilE': nilpotent E^`(1) := der1_sigma_compl_nil maxM hallE. have nsE'piE pi: 'O_pi(E^`(1)) <| E by rewrite !gFnormal_trans. have SylowE3 P: Sylow E3 P -> [/\ cyclic P, P \subset E^`(1) & 'C_P(E) = 1]. - case/SylowP=> p p_pr sylP; have [sPE3 pP _] := and3P sylP. have [-> | ntP] := eqsVneq P 1. by rewrite cyclic1 sub1G (setIidPl (sub1G _)). have t3p: p \in \tau3(M). rewrite (pnatPpi t3E3) // -p_rank_gt0 -(p_rank_Sylow sylP) -rank_pgroup //. by rewrite rank_gt0. have sPE: P \subset E := subset_trans sPE3 sE3E. have cycP: cyclic P. rewrite (odd_pgroup_rank1_cyclic pP) ?mFT_odd //. rewrite (tau3E maxM hallE) in t3p. by case/andP: t3p => _ /eqP <-; rewrite p_rankS. have nEp'E: E \subset 'N('O_p^'(E)) by apply: gFnorm. have nEp'P := subset_trans sPE nEp'E. have sylP_E := subHall_Sylow hallE3 t3p sylP. have nsEp'P_E: 'O_p^'(E) <*> P <| E. rewrite sub_der1_normal ?join_subG ?pcore_sub //=. rewrite norm_joinEr // -quotientSK ?gFsub_trans //=. have [_ /= <- _ _] := dprodP (nilpotent_pcoreC p nilE'). rewrite -quotientMidr -mulgA (mulSGid (pcore_max _ _)) ?pcore_pgroup //=. rewrite quotientMidr quotientS //. apply: subset_trans (pcore_sub_Hall sylP_E). by rewrite pcore_max ?pcore_pgroup ?nsE'piE. have nEP_sol: solvable 'N_E(P) by rewrite (solvableS _ solE) ?subsetIl. have [K hallK] := Hall_exists p^' nEP_sol; have [sKNEP p'K _] := and3P hallK. have coPK: coprime #|P| #|K| := pnat_coprime pP p'K. have sP_NEP: P \subset 'N_E(P) by rewrite subsetI sPE normG. have mulPK: P * K = 'N_E(P). apply/eqP; rewrite eqEcard mul_subG //= coprime_cardMg // (card_Hall hallK). by rewrite (card_Hall (pHall_subl sP_NEP (subsetIl E _) sylP_E)) partnC. have{sKNEP} [sKE nPK] := subsetIP sKNEP; have nEp'K := subset_trans sKE nEp'E. have defE: 'O_p^'(E) <*> K * P = E. have sP_Ep'P: P \subset 'O_p^'(E) <*> P := joing_subr _ _. have sylP_Ep'P := pHall_subl sP_Ep'P (normal_sub nsEp'P_E) sylP_E. rewrite -{2}(Frattini_arg nsEp'P_E sylP_Ep'P) /= !norm_joinEr //. by rewrite -[LHS]mulgA (normC nPK) -mulPK -{1}(mulGid P) !mulgA. have ntPE': P :&: E^`(1) != 1. have sylPE' := Hall_setI_normal (der_normal 1 E) sylP_E. rewrite -rank_gt0 (rank_Sylow sylPE') p_rank_gt0. by rewrite (tau3E maxM hallE) in t3p; case/andP: t3p. have defP := coprime_abelian_cent_dprod nPK coPK (cyclic_abelian cycP). have{defP} [[PK1 _]|[regKP defP]] := cyclic_pgroup_dprod_trivg pP cycP defP. have coP_Ep'K: coprime #|P| #|'O_p^'(E) <*> K|. rewrite (pnat_coprime pP) // -pgroupE norm_joinEr //. by rewrite pgroupM pcore_pgroup. rewrite -subG1 -(coprime_TIg coP_Ep'K) setIS ?der1_min // in ntPE'. rewrite -{1}defE mulG_subG normG normsY // cents_norm //. exact/commG1P. by rewrite -{2}defE quotientMidl quotient_abelian ?cyclic_abelian. split=> //; first by rewrite -defP commgSS. by apply/trivgP; rewrite -regKP setIS ?centS. have sE3E': E3 \subset E^`(1). by rewrite -(Sylow_gen E3) gen_subG; apply/bigcupsP=> P; case/SylowE3. have cycE3: cyclic E3. rewrite nil_Zgroup_cyclic ?(nilpotentS sE3E') //. by apply/forall_inP => P; case/SylowE3. have regEE3: 'C_E3(E) = 1. have [// | [p p_pr]] := trivgVpdiv 'C_E3(E). case/Cauchy=> // x /setIP[]; rewrite -!cycle_subG => sXE3 cEX ox. have pX: p.-elt x by rewrite /p_elt ox pnat_id. have [P sylP sXP] := Sylow_superset sXE3 pX. suffices: <[x]> == 1 by case/idPn; rewrite cycle_eq1 -order_gt1 ox prime_gt1. rewrite -subG1; case/SylowE3: (p_Sylow sylP) => _ _ <-. by rewrite subsetI sXP. have nsE3E: E3 <| E. have hallE3_E' := pHall_subl sE3E' (der_sub 1 E) hallE3. by rewrite (nilpotent_Hall_pcore nilE' hallE3_E') /=. have [sE2E t2E2 _] := and3P hallE2; have [_ nE3E] := andP nsE3E. have coE21: coprime #|E2| #|E1| := sub_pnat_coprime tau2'1 t2E2 t1E1. have coE31: coprime #|E3| #|E1| := sub_pnat_coprime tau3'1 t3E3 t1E1. have coE32: coprime #|E3| #|E2| := sub_pnat_coprime tau3'2 t3E3 t2E2. have{groupE21} defE: E3 ><| (E2 ><| E1) = E. have defE21: E2 * E1 = E2 <*> E1 by rewrite -genM_join gen_set_id. have sE21E: E2 <*> E1 \subset E by rewrite join_subG sE2E. have nE3E21 := subset_trans sE21E nE3E. have coE312: coprime #|E3| #|E2 <*> E1|. by rewrite -defE21 coprime_cardMg // coprimeMr coE32. have nE21: E1 \subset 'N(E2). rewrite (subset_trans (joing_subr E2 E1)) ?sub_der1_norm ?joing_subl //. rewrite /= -{2}(mulg1 E2) -(setIidPr (der_sub 1 _)) /=. rewrite -(coprime_mulG_setI_norm defE21) ?gFnorm //. by rewrite mulgSS ?subsetIl // -tiE'E1 setIC setSI ?dergS. rewrite (sdprodEY nE21) ?sdprodE ?coprime_TIg //=. apply/eqP; rewrite eqEcard mul_subG // coprime_cardMg //= -defE21. rewrite -(partnC \tau3(M) (cardG_gt0 E)) (card_Hall hallE3) leq_mul //. rewrite coprime_cardMg // (card_Hall hallE1) (card_Hall hallE2). rewrite -[#|E|`__](partnC \tau2(M)) ?leq_mul ?(partn_part _ tau3'2) //. rewrite -partnI dvdn_leq // sub_in_partn // => p piEp; apply/implyP. rewrite inE /= -negb_or /= orbC implyNb orbC. by rewrite -(partition_pi_sigma_compl maxM hallE). split=> // [/eqP E2_1|]; last split=> //. apply: contraTneq (sol_der1_proper solM (subxx _) (mmax_neq1 maxM)) => E1_1. case/sdprodP: (sdprod_sigma maxM hallE) => _ defM _ _. rewrite properE der_sub /= negbK -{1}defM mulG_subG Msigma_der1 //. by rewrite -defE E1_1 E2_1 !sdprodg1 (subset_trans sE3E') ?dergS //. case/sdprodP: defE => [[_ E21 _ defE21]]; rewrite defE21 => defE nE321 tiE321. have{defE21} [_ defE21 nE21 tiE21] := sdprodP defE21. have [nE32 nE31] := (subset_trans sE2E nE3E, subset_trans sE1E nE3E). rewrite [E3 ><| _]sdprodEY ? sdprodE ?coprime_TIg ?normsY //=. by rewrite norm_joinEr // -mulgA defE21. by rewrite norm_joinEr // coprime_cardMg // coprimeMl coE31. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq choice div fintype) mathcomp(path bigop finset prime fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor pgroup cyclic commutator) mathcomp(center gseries nilpotent sylow abelian maximal hall frobenius) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9 BGsection10 BGsection11)