proposition: Lemma cent_Malpha_reg_tau1 M p q P Q (Ma := M`_\alpha) : M \in 'M -> p \in \tau1(M) -> q \in p^' -> P \in 'E_p^1(M) -> Q :!=: 1 -> P \subset 'N(Q) -> 'C_Q(P) = 1 -> 'M('N(Q)) != [set M] -> [/\ Ma != 1 -> q \notin \alpha(M) -> q.-group Q -> Q \subset M -> 'C_Ma(P) != 1 /\ 'C_Ma(Q <*> P) = 1 & q.-Sylow(M) Q -> [/\ \alpha(M) =i \beta(M), Ma != 1, q \notin \alpha(M), 'C_Ma(P) != 1 & 'C_Ma(Q <*> P) = 1]].
proof: Proof. move=> maxM t1p p'q EpP ntQ nQP regPQ nonuniqNQ. set QP := Q <*> P; set CaQP := 'C_Ma(QP); set part_a := _ -> _. have ssolM := solvableS _ (mmax_sol maxM). have [sPM abelP oP] := pnElemPcard EpP; have{abelP} [pP _] := andP abelP. have p_pr := pnElem_prime EpP; have [s'p _] := andP t1p. have a'p: p \in \alpha(M)^' by apply: contra s'p; apply: alpha_sub_sigma. have{a'p} [a'P t2'p] := (pi_pgroup pP a'p, tau2'1 t1p). have uniqCMX: 'M('C_M(_)) = [set M] := def_uniq_mmax _ maxM (subsetIl _ _). have nQ_CMQ: 'C_M(Q) \subset 'N(Q) by rewrite setIC subIset ?cent_sub. have part_a_holds: part_a. move=> ntMa a'q qQ sQM; have{p'q} p'Q := pi_pgroup qQ p'q. have{p'Q} coQP: coprime #|Q| #|P| by rewrite coprime_sym (pnat_coprime pP). have{a'q} a'Q: \alpha(M)^'.-group Q by rewrite (pi_pgroup qQ). have rCMaQle1: 'r('C_Ma(Q)) <= 1. rewrite leqNgt; apply: contra nonuniqNQ => rCMaQgt1; apply/eqP. apply: def_uniq_mmaxS (uniqCMX Q _) => //; last exact: cent_alpha'_uniq. exact: mFT_norm_proper (mFT_pgroup_proper qQ). have rCMaPle1: 'r('C_Ma(P)) <= 1. have: ~~ ('N(P) \subset M). by apply: contra (prime_class_mmax_norm maxM pP) _; apply/norP. rewrite leqNgt; apply: contra => rCMaPgt1. apply: (sub_uniq_mmax (uniqCMX P _)); first exact: cent_alpha'_uniq. by rewrite /= setIC subIset ?cent_sub. exact: mFT_norm_proper (nt_pnElem EpP _) (mFT_pgroup_proper pP). have [sMaM nMaM] := andP (pcore_normal _ M : Ma <| M). have aMa: \alpha(M).-group Ma by rewrite pcore_pgroup. have nMaQP: QP \subset 'N(Ma) by rewrite join_subG !(subset_trans _ nMaM). have{nMaM} coMaQP: coprime #|Ma| #|QP|. by rewrite (pnat_coprime aMa) ?[QP]norm_joinEr // [pnat _ _]pgroupM ?a'Q. pose r := pdiv #|if CaQP == 1 then Ma else CaQP|. have{ntMa} piMar: r \in \pi(Ma). rewrite /r; case: ifPn => [_| ntCaQP]; first by rewrite pi_pdiv cardG_gt1. by rewrite (piSg (subsetIl Ma 'C(QP))) // pi_pdiv cardG_gt1. have{aMa} a_r: r \in \alpha(M) := pnatPpi aMa piMar. have [r'Q r'P] : r^'.-group Q /\ r^'.-group P by rewrite !(pi'_p'group _ a_r). have [Rc /= sylRc] := Sylow_exists r [group of CaQP]. have [sRcCaQP rRc _] := and3P sylRc; have [sRcMa cQPRc] := subsetIP sRcCaQP. have nRcQP: QP \subset 'N(Rc) by rewrite cents_norm // centsC. have{nMaQP rRc coMaQP sRcCaQP sRcMa nRcQP} [R [sylR nR_QP sRcR]] := coprime_Hall_subset nMaQP coMaQP (ssolM _ sMaM) sRcMa rRc nRcQP. have{nR_QP} [[sRMa rR _] [nRQ nRP]] := (and3P sylR, joing_subP nR_QP). have{piMar} ntR: R :!=: 1 by rewrite -rank_gt0 (rank_Sylow sylR) p_rank_gt0. have [r_pr _ _] := pgroup_pdiv rR ntR. have sylR_M := subHall_Sylow (Malpha_Hall maxM) a_r sylR. have{rCMaQle1 a_r} not_cRQ: ~~ (Q \subset 'C(R)). apply: contraL rCMaQle1; rewrite centsC => cQR; rewrite -ltnNge ltnW //. by rewrite (leq_trans a_r) // -(rank_Sylow sylR_M) rankS // subsetI sRMa. have [R1 [charR1 _ _ expR1 rCR1_AutR]] := critical_odd rR (mFT_odd R) ntR. have [sR1R nR1R] := andP (char_normal charR1); have rR1 := pgroupS sR1R rR. have [nR1P nR1Q] := (char_norm_trans charR1 nRP, char_norm_trans charR1 nRQ). have [coR1Q coR1P] := (pnat_coprime rR1 r'Q, pnat_coprime rR1 r'P). have {rCR1_AutR not_cRQ} not_cR1Q: ~~ (Q \subset 'C(R1)). apply: contra not_cRQ => cR1Q; rewrite -subsetIidl. rewrite -quotient_sub1 ?normsI ?normG ?norms_cent // subG1 trivg_card1. rewrite (pnat_1 _ (quotient_pgroup _ r'Q)) //= -ker_conj_aut. rewrite (card_isog (first_isog_loc _ _)) //; apply: pgroupS rCR1_AutR. apply/subsetP=> za; case/morphimP=> z nRz Qz ->; rewrite inE Aut_aut inE. apply/subsetP=> x R1x; rewrite inE [_ x _]norm_conj_autE ?(subsetP sR1R) //. by rewrite /conjg -(centsP cR1Q z) ?mulKg. pose R0 := 'C_R1(Q); have sR0R1: R0 \subset R1 := subsetIl R1 'C(Q). have nR0P: P \subset 'N(R0) by rewrite normsI ?norms_cent. have nR0Q: Q \subset 'N(R0) by rewrite normsI ?norms_cent ?normG. pose R1Q := R1 <*> Q; have defR1Q: R1 * Q = R1Q by rewrite -norm_joinEr. have [[sR1_R1Q sQ_R1Q] tiR1Q] := (joing_sub (erefl R1Q), coprime_TIg coR1Q). have not_nilR1Q: ~~ nilpotent R1Q. by apply: contra not_cR1Q => /sub_nilpotent_cent2; apply. have not_nilR1Qb: ~~ nilpotent (R1Q / R0). apply: contra not_cR1Q => nilR1Qb. have [nilR1 solR1] := (pgroup_nil rR1, pgroup_sol rR1). rewrite centsC -subsetIidl -(nilpotent_sub_norm nilR1 sR0R1) //= -/R0. rewrite -(quotientSGK (subsetIr R1 _)) ?coprime_quotient_cent //= -/R0. rewrite quotientInorm subsetIidl /= centsC -/R0. by rewrite (sub_nilpotent_cent2 nilR1Qb) ?quotientS ?coprime_morph. have coR1QP: coprime #|R1Q| #|P|. by rewrite -defR1Q TI_cardMg // coprimeMl coR1P. have defR1QP: R1Q ><| P = R1Q <*> P. by rewrite sdprodEY ?normsY ?coprime_TIg. have sR1Ma := subset_trans sR1R sRMa; have sR1M := subset_trans sR1Ma sMaM. have solR1Q: solvable R1Q by rewrite ssolM // !join_subG sR1M. have solR1QP: solvable (R1Q <*> P) by rewrite ssolM // !join_subG sR1M sQM. have defCR1QP: 'C_R1Q(P) = 'C_R1(P). by rewrite -defR1Q -subcent_TImulg ?regPQ ?mulg1 //; apply/subsetIP. have ntCR1P: 'C_R1(P) != 1. apply: contraNneq not_nilR1Q => regPR1. by rewrite (prime_Frobenius_sol_kernel_nil defR1QP) ?oP ?defCR1QP. split; first exact: subG1_contra (setSI _ sR1Ma) ntCR1P. have{rCMaPle1} cycCRP: cyclic 'C_R(P). have rCRP: r.-group 'C_R(P) := pgroupS (subsetIl R _) rR. rewrite (odd_pgroup_rank1_cyclic rCRP) ?mFT_odd -?rank_pgroup {rCRP}//. by rewrite (leq_trans (rankS _) rCMaPle1) ?setSI. have{ntCR1P} oCR1P: #|'C_R1(P)| = r. have cycCR1P: cyclic 'C_R1(P) by rewrite (cyclicS _ cycCRP) ?setSI. apply: cyclic_abelem_prime ntCR1P => //. by rewrite abelemE ?cyclic_abelian // -expR1 exponentS ?subsetIl. apply: contraNeq not_nilR1Qb => ntCaQP. have{Rc sRcR sylRc cQPRc ntCaQP} ntCRQP: 'C_R(QP) != 1. suffices: Rc :!=: 1 by apply: subG1_contra; apply/subsetIP. rewrite -rank_gt0 (rank_Sylow sylRc) p_rank_gt0. by rewrite /r (negPf ntCaQP) pi_pdiv cardG_gt1. have defR1QPb: (R1Q / R0) ><| (P / R0) = R1Q <*> P / R0. have [_ <- nR1QP _] := sdprodP defR1QP; rewrite quotientMr //. by rewrite sdprodE ?quotient_norms // coprime_TIg ?coprime_morph. have tiPR0: R0 :&: P = 1 by rewrite coprime_TIg // (coprimeSg sR0R1). have prPb: prime #|P / R0| by rewrite -(card_isog (quotient_isog _ _)) ?oP. rewrite (prime_Frobenius_sol_kernel_nil defR1QPb) ?quotient_sol //. rewrite -coprime_quotient_cent ?(subset_trans sR0R1) // quotientS1 //=. rewrite defCR1QP -{2}(setIidPl sR1R) -setIA subsetI subsetIl. apply: subset_trans (setIS R (centS (joing_subl Q P))). rewrite -(cardSg_cyclic cycCRP) ?setIS ?setSI ?centS ?joing_subr // oCR1P. by have [_ -> _] := pgroup_pdiv (pgroupS (subsetIl R _) rR) ntCRQP. split=> // sylQ; have [sQM qQ _] := and3P sylQ. have ltQG := mFT_pgroup_proper qQ; have ltNQG := mFT_norm_proper ntQ ltQG. have{p'q} p'Q := pi_pgroup qQ p'q. have{p'Q} coQP: coprime #|Q| #|P| by rewrite coprime_sym (pnat_coprime pP). have sQM': Q \subset M^`(1). by rewrite -(coprime_cent_prod nQP) ?ssolM // regPQ mulg1 commgSS. have ntMa: Ma != 1. apply: contraNneq nonuniqNQ => Ma1. rewrite (mmax_normal maxM _ ntQ) ?mmax_sup_id //. have sylQ_M': q.-Sylow(M^`(1)) Q := pHall_subl sQM' (der_sub 1 M) sylQ. rewrite (nilpotent_Hall_pcore _ sylQ_M') ?gFnormal_trans //. by rewrite (isog_nil (quotient1_isog _)) -Ma1 Malpha_quo_nil. have a'q: q \notin \alpha(M). apply: contra nonuniqNQ => a_q. have uniqQ: Q \in 'U by rewrite rank3_Uniqueness ?(rank_Sylow sylQ). by rewrite (def_uniq_mmaxS _ _ (def_uniq_mmax _ _ sQM)) ?normG. have b'q := contra (@beta_sub_alpha _ M _) a'q. case: part_a_holds => // ntCaP regQP; split=> {ntCaP regQP}// r. apply/idP/idP=> [a_r | ]; last exact: beta_sub_alpha. apply: contraR nonuniqNQ => b'r; apply/eqP. apply: def_uniq_mmaxS (uniqCMX Q _) => //. have q'r: r != q by apply: contraNneq a'q => <-. by have [|_ -> //] := beta'_cent_Sylow maxM b'r b'q qQ; rewrite q'r sQM'. 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)