proposition: Lemma primes_norm_tau2Elem M E p A Mstar : M \in 'M -> \sigma(M)^'.-Hall(M) E -> p \in \tau2(M) -> A \in 'E_p^2(E) -> Mstar \in 'M('N(A)) -> [/\ {subset \tau2(M) <= [predD \sigma(Mstar) & \beta(Mstar)]}, [predU \tau1(Mstar) & \tau2(Mstar)].-group (E / 'C_E(A)) & forall q, q \in \pi(E / 'C_E(A)) -> q \in \pi('C_E(A)) -> [/\ q \in \tau2(Mstar), exists2 P, P \in 'Syl_p(G) & P <| Mstar & exists Q, [/\ Q \in 'Syl_q(G), Q \subset Mstar & abelian Q]]].
proof: Proof. move=> maxM hallE t2Mp Ep2A; move: Mstar. have [sAE abelA dimA] := pnElemP Ep2A; have [pA cAA _] := and3P abelA. have ntA: A :!=: 1 by apply: (nt_pnElem Ep2A). have [sEM solE] := (pHall_sub hallE, sigma_compl_sol hallE). have [_ nsCA_E t1CEAb] := tau1_cent_tau2Elem_factor maxM hallE t2Mp Ep2A. have [sAM nCA_E] := (subset_trans sAE sEM, normal_norm nsCA_E). have part_a H: H \in 'M('N(A)) -> {subset \tau2(M) <= [predD \sigma(H) & \beta(H)]}. - case/setIdP=> maxH sNA_H q t2Mq. have sCA_H: 'C(A) \subset H := subset_trans (cent_sub A) sNA_H. have sAH := subset_trans cAA sCA_H. have sHp: p \in \sigma(H). have [// | t2Hp] := orP (prime_class_mmax_norm maxH pA sNA_H). apply: contraLR sNA_H => sH'p. have sH'A: \sigma(H)^'.-group A by apply: pi_pnat pA _. have [F hallF sAF] := Hall_superset (mmax_sol maxH) sAH sH'A. have Ep2A_F: A \in 'E_p^2(F) by apply/pnElemP. by have [_ [_ _ ->]]:= tau2_compl_context maxH hallF t2Hp Ep2A_F. rewrite inE /= -predI_sigma_beta //= negb_and /= orbC. have [-> /= _] := tau2_not_beta maxM t2Mq. have [B Eq2B]: exists B, B \in 'E_q^2('C(A)). have [E2 hallE2 sAE2] := Hall_superset solE sAE (pi_pnat pA t2Mp). have cE2E2: abelian E2 := tau2_compl_abelian maxM hallE hallE2. have [Q sylQ] := Sylow_exists q E2; have sQE2 := pHall_sub sylQ. have sylQ_E := subHall_Sylow hallE2 t2Mq sylQ. apply/p_rank_geP; apply: leq_trans (p_rankS q (centsS sAE2 cE2E2)). rewrite -(p_rank_Sylow sylQ) (p_rank_Sylow sylQ_E). by move: t2Mq; rewrite (tau2E hallE) => /andP[_ /eqP->]. have [cAB abelB dimB] := pnElemP Eq2B; have sBH := subset_trans cAB sCA_H. have{} Eq2B: B \in 'E_q^2(H) by apply/pnElemP. have rqHgt1: 'r_q(H) > 1 by apply/p_rank_geP; exists B. have piHq: q \in \pi(H) by rewrite -p_rank_gt0 ltnW. rewrite partition_pi_mmax // in piHq. case/or4P: piHq rqHgt1 => // [|t2Hq _|]; try by case/and3P=> _ /eqP->. have [_ _ regB _ _] := tau2_context maxH t2Hq Eq2B. case/negP: ntA; rewrite -subG1 -regB subsetI centsC cAB andbT. by rewrite (sub_Hall_pcore (Msigma_Hall maxH)) // (pi_pgroup pA). have part_b H: H \in 'M('N(A)) -> [predU \tau1(H) & \tau2(H)].-group (E / 'C_E(A)). - move=> maxNA_H; have [maxH sNA_H] := setIdP maxNA_H. have [/= bH'p sHp] := andP (part_a H maxNA_H p t2Mp). have sCA_H: 'C(A) \subset H := subset_trans (cent_sub A) sNA_H. have sAH := subset_trans cAA sCA_H. apply/pgroupP=> q q_pr q_dv_CEAb; apply: contraR bH'p => t12H'q. have [Q sylQ] := Sylow_exists q E; have [sQE qQ _] := and3P sylQ. have nsAE: A <| E by case/(tau2_compl_context maxM): Ep2A => //; case. have nAE := normal_norm nsAE; have nAQ := subset_trans sQE nAE. have sAQ_A: [~: A, Q] \subset A by rewrite commg_subl. have ntAQ: [~: A, Q] != 1. apply: contraTneq q_dv_CEAb => /commG1P cAQ. have nCEA_Q := subset_trans sQE nCA_E. rewrite -p'natE // -partn_eq1 ?cardg_gt0 //. rewrite -(card_Hall (quotient_pHall nCEA_Q sylQ)) -trivg_card1 -subG1. by rewrite quotient_sub1 // subsetI sQE centsC. have sQH: Q \subset H := subset_trans nAQ sNA_H. have sHsubH' r X: r \in \sigma(H) -> X \subset H -> r.-group X -> X \subset H^`(1). + move=> sHr sXH rX; apply: subset_trans (Msigma_der1 maxH). by rewrite (sub_Hall_pcore (Msigma_Hall maxH)) // (pi_pgroup rX sHr). have sAH': A \subset H^`(1) by apply: sHsubH' pA. have{t12H'q} sQH': Q \subset H^`(1). have [sHq | sH'q] := boolP (q \in \sigma(H)); first exact: sHsubH' qQ. have{sH'q} sH'Q: \sigma(H)^'.-group Q by apply: (pi_pnat qQ). have{sH'Q} [F hallF sQF] := Hall_superset (mmax_sol maxH) sQH sH'Q. have [-> | ntQ] := eqsVneq Q 1; first exact: sub1G. have{t12H'q} t3Hq: q \in \tau3(H). apply: implyP t12H'q; rewrite implyNb -orbA. rewrite -(partition_pi_sigma_compl maxH hallF) -p_rank_gt0. by rewrite (leq_trans _ (p_rankS q sQF)) // -rank_pgroup // rank_gt0. have solF: solvable F := sigma_compl_sol hallF. have [F3 hallF3 sQF3] := Hall_superset solF sQF (pi_pnat qQ t3Hq). have [[F1 hallF1] _] := ex_tau13_compl hallF. have [F2 _ complFi] := ex_tau2_compl hallF hallF1 hallF3. have [[sF3H' _] _ _ _ _] := sigma_compl_context maxH complFi. exact: subset_trans sQF3 (subset_trans sF3H' (dergS 1 (pHall_sub hallF))). have hallHb: \beta(H).-Hall(H) H`_\beta := Mbeta_Hall maxH. have nilH'b: nilpotent (H^`(1) / H`_\beta) := Mbeta_quo_nil maxH. have{nilH'b} sAQ_Hb: [~: A, Q] \subset H`_\beta. rewrite commGC -quotient_cents2 ?gFnorm_trans ?normsG //=. rewrite (sub_nilpotent_cent2 nilH'b) ?quotientS ?coprime_morph //. rewrite (pnat_coprime (pi_pnat pA t2Mp) (pi_pnat qQ _)) ?tau2'1 //. by rewrite (pnatPpi t1CEAb) // mem_primes q_pr cardG_gt0. rewrite (pnatPpi (pHall_pgroup hallHb)) // (piSg sAQ_Hb) // -p_rank_gt0. by rewrite -(rank_pgroup (pgroupS sAQ_A pA)) rank_gt0. move=> H maxNA_H; split; last 1 [move=> q piCEAb_q piCEAq] || by auto. have [_ sHp]: _ /\ p \in \sigma(H) := andP (part_a H maxNA_H p t2Mp). have{maxNA_H} [maxH sNA_H] := setIdP maxNA_H. have{sNA_H} sCA_H: 'C(A) \subset H := subset_trans (cent_sub A) sNA_H. have{piCEAq} [Q0 EqQ0]: exists Q0, Q0 \in 'E_q^1('C_E(A)). by apply/p_rank_geP; rewrite p_rank_gt0. have [sQ0_CEA abelQ0 dimQ0]:= pnElemP EqQ0; have [qQ0 cQ0Q0 _] := and3P abelQ0. have{sQ0_CEA} [sQ0E cAQ0]: Q0 \subset E /\ Q0 \subset 'C(A). by apply/andP; rewrite -subsetI. have ntQ0: Q0 :!=: 1 by apply: (nt_pnElem EqQ0). have{t1CEAb} t1Mq: q \in \tau1(M) := pnatPpi t1CEAb piCEAb_q. have [Q sylQ sQ0Q] := Sylow_superset sQ0E qQ0; have [sQE qQ _] := and3P sylQ. have [E1 hallE1 sQE1] := Hall_superset solE sQE (pi_pnat qQ t1Mq). have rqE: 'r_q(E) = 1%N. by move: t1Mq; rewrite (tau1E maxM hallE) andbA andbC; case: eqP. have cycQ: cyclic Q. by rewrite (odd_pgroup_rank1_cyclic qQ) ?mFT_odd // (p_rank_Sylow sylQ) rqE. have sCAE: 'C(A) \subset E by case/(tau2_compl_context maxM): Ep2A => // _ []. have{sCAE} sylCQA: q.-Sylow('C(A)) 'C_Q(A). by apply: Hall_setI_normal sylQ; rewrite /= -(setIidPr sCAE). have{sylCQA} defNA: 'C(A) * 'N_('N(A))(Q0) = 'N(A). apply/eqP; rewrite eqEsubset mulG_subG cent_sub subsetIl /=. rewrite -{1}(Frattini_arg (cent_normal A) sylCQA) mulgS ?setIS ?char_norms //. by rewrite (sub_cyclic_char Q0 (cyclicS (subsetIl Q _) cycQ)) subsetI sQ0Q. have [L maxNQ0_L]: {L | L \in 'M('N(Q0))}. by apply: mmax_exists; rewrite mFT_norm_proper ?(mFT_pgroup_proper qQ0). have{maxNQ0_L} [maxL sNQ0_L] := setIdP maxNQ0_L. have sCQ0_L: 'C(Q0) \subset L := subset_trans (cent_sub Q0) sNQ0_L. have sAL: A \subset L by rewrite (subset_trans _ sCQ0_L) // centsC. have sCA_L: 'C(A) \subset L. by have /p2Elem_mmax[]: A \in 'E_p^2(L) by apply/pnElemP. have{sCA_L defNA} maxNA_L: L \in 'M('N(A)). by rewrite inE maxL -defNA setIC mul_subG // subIset ?sNQ0_L. have t2Lq: q \in \tau2(L). have /orP[sLq | //] := prime_class_mmax_norm maxL qQ0 sNQ0_L. by have /orP[/andP[/negP] | ] := pnatPpi (part_b L maxNA_L) piCEAb_q. have [cQQ [/= sL'q _]] := (cyclic_abelian cycQ, andP t2Lq). have sQL: Q \subset L := subset_trans (centsS sQ0Q cQQ) sCQ0_L. have [F hallF sQF] := Hall_superset (mmax_sol maxL) sQL (pi_pnat qQ sL'q). have [B Eq2B _] := ex_tau2Elem hallF t2Lq. have [_ sLp]: _ /\ p \in \sigma(L) := andP (part_a L maxNA_L p t2Mp). have{H sHp maxH sCA_H} <-: L :=: H. have sLHp: p \in [predI \sigma(L) & \sigma(H)] by apply/andP. have [_ transCA _] := sigma_group_trans maxH sHp pA. set S := finset _ in transCA; have sAH := subset_trans cAA sCA_H. suffices [SH SL]: gval H \in S /\ gval L \in S. have [c cAc -> /=]:= atransP2 transCA SH SL. by rewrite conjGid // (subsetP sCA_H). have [_ _ _ TIsL] := tau2_compl_context maxL hallF t2Lq Eq2B. apply/andP; rewrite !inE sAH sAL orbit_refl orbit_sym /= andbT. by apply: contraLR sLHp => /TIsL[] // _ ->. split=> //. exists ('O_p(L`_\sigma))%G; last by rewrite /= -pcoreI pcore_normal. rewrite inE (subHall_Sylow (Msigma_Hall_G maxL) sLp) //. by rewrite nilpotent_pcore_Hall // (tau2_Msigma_nil maxL t2Lq). have [Q1 sylQ1 sQQ1] := Sylow_superset (subsetT Q) qQ. have [sQ0Q1 qQ1] := (subset_trans sQ0Q sQQ1, pHall_pgroup sylQ1). have [cQ1Q1 | not_cQ1Q1] := boolP (abelian Q1). by exists Q1; rewrite inE (subset_trans (centsS sQ0Q1 cQ1Q1)). have [_ _ regB [F0 /=]] := nonabelian_tau2 maxL hallF t2Lq Eq2B qQ1 not_cQ1Q1. have{regB} ->: 'C_B(L`_\sigma) = Q0; last move=> defF _. apply: contraTeq sCQ0_L => neqQ0B; case: (regB Q0) => //. by rewrite 2!inE eq_sym neqQ0B; apply/pnElemP; rewrite (subset_trans sQ0Q). have{defF} defQ: Q0 \x (F0 :&: Q) = Q. rewrite dprodEsd ?(centSS (subsetIr F0 Q) sQ0Q) //. by rewrite (sdprod_modl defF sQ0Q) (setIidPr sQF). have [[/eqP/idPn//] | [_ eqQ0Q]] := cyclic_pgroup_dprod_trivg qQ cycQ defQ. have nCEA_Q := subset_trans sQE nCA_E. case/idPn: piCEAb_q; rewrite -p'natEpi -?partn_eq1 ?cardG_gt0 //. rewrite -(card_Hall (quotient_pHall nCEA_Q sylQ)) -trivg_card1 -subG1. by rewrite quotient_sub1 // subsetI sQE -eqQ0Q. 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)