proposition: Theorem FTtypeF_complement M (Ms := M`_\sigma) E U : M \in 'M -> \sigma(M)^'.-Hall(M) E -> Hall E U -> U <| E -> U :!=: 1 -> {in U^#, forall e, [predU \tau1(M) & \tau3(M)].-elt e -> 'C_Ms[e] = 1} -> [/\ exists A0 : {group gT}, [/\ A0 <| U, abelian A0 & {in Ms^#, forall x, 'C_U[x] \subset A0}] & exists E0 : {group gT}, [/\ E0 \subset U, exponent E0 = exponent U & [Frobenius Ms <*> E0 = Ms ><| E0]]].
proof: Proof. set p13 := predU _ _ => maxM hallE /Hall_pi hallU nsUE ntU regU13. have [[E1 hallE1] [E3 hallE3]] := ex_tau13_compl hallE. have [E2 hallE2 complEi] := ex_tau2_compl hallE hallE1 hallE3. have [[sE1E _] [sE2E t2E2 _]] := (andP hallE1, and3P hallE2). have [[_ nsE3E] _ [cycE1 _] [defE _] _] := sigma_compl_context maxM complEi. have [[[sE3E t3E3 _][_ nE3E]] [sUE _]] := (and3P hallE3, andP nsE3E, andP nsUE). have defM: Ms ><| E = M := sdprod_sigma maxM hallE. have [nsMsM sEM mulMsE nMsE tiMsE] := sdprod_context defM. have ntMs: Ms != 1 := Msigma_neq1 maxM. have{defM} defMsU: Ms ><| U = Ms <*> U := sdprod_subr defM sUE. pose U2 := (E2 :&: U)%G. have hallU2: \tau2(M).-Hall(U) U2 := Hall_setI_normal nsUE hallE2. have [U2_1 | ntU2] := eqsVneq U2 1. have frobMsU: [Frobenius Ms <*> U = Ms ><| U]. apply/Frobenius_semiregularP=> // e Ue. apply: regU13 => //; case/setD1P: Ue => _; apply: mem_p_elt. have: \tau2(M)^'.-group U. by rewrite -partG_eq1 -(card_Hall hallU2) U2_1 cards1. apply: sub_in_pnat => p /(piSg sUE). by rewrite (partition_pi_sigma_compl maxM hallE) orbCA => /orP[] // /idPn. split; [exists 1%G; rewrite normal1 abelian1 | by exists U]. by split=> //= x Ux; rewrite (Frobenius_reg_compl frobMsU). have [[sU2U t2U2 _] [p p_pr rU2]] := (and3P hallU2, rank_witness U2). have piU2p: p \in \pi(U2) by rewrite -p_rank_gt0 -rU2 rank_gt0. have t2p: p \in \tau2(M) := pnatPpi t2U2 piU2p. have [A Ep2A Ep2A_M] := ex_tau2Elem hallE t2p. have [sAE abelA _] := pnElemP Ep2A; have{abelA} [pA cAA _] := and3P abelA. have [S sylS sAS] := Sylow_superset (subsetT A) pA. have [cSS | not_cSS] := boolP (abelian S); last first. have [_] := nonabelian_tau2 maxM hallE t2p Ep2A (pHall_pgroup sylS) not_cSS. set A0 := ('C_A(_))%G => [] [oA0 _] _ {defE} [E0 defE regE0]. have [nsA0E sE0E mulAE0 nAE0 tiAE0] := sdprod_context defE. have [P sylP] := Sylow_exists p U; have [sPU _] := andP sylP. have sylP_E := subHall_Sylow hallU (piSg sU2U piU2p) sylP. have pA0: p.-group A0 by rewrite /pgroup oA0 pnat_id. have sA0P: A0 \subset P. by apply: subset_trans (pcore_sub_Hall sylP_E); apply: pcore_max. have sA0U: A0 \subset U := subset_trans sA0P sPU. pose U0 := (E0 :&: U)%G. have defU: A0 ><| U0 = U by rewrite (sdprod_modl defE) // (setIidPr sUE). have piU0p: p \in \pi(U0). have:= lognSg p sAE; rewrite (card_pnElem Ep2A) pfactorK //. rewrite -logn_part -(card_Hall sylP_E) (card_Hall sylP) logn_part. rewrite -(sdprod_card defU) oA0 lognM // ?prime_gt0 // logn_prime // eqxx. by rewrite ltnS logn_gt0. have defM0: Ms ><| U0 = Ms <*> U0 := sdprod_subr defMsU (subsetIr _ _). have frobM0: [Frobenius Ms <*> U0 = Ms ><| U0]. apply/Frobenius_semiregularP=> // [|e /setD1P[nte /setIP[E0e Ue]]]. by rewrite -rank_gt0 (leq_trans _ (p_rank_le_rank p _)) ?p_rank_gt0. have [ | ] := boolP (p13.-elt e); first by apply: regU13; rewrite !inE nte. apply: contraNeq => /trivgPn[x /setIP[Ms_x cex] ntx]. apply/pgroupP=> q q_pr q_dv_x; rewrite inE /= (regE0 x) ?inE ?ntx //. rewrite mem_primes q_pr cardG_gt0 (dvdn_trans q_dv_x) ?order_dvdG //. by rewrite inE E0e cent1C. have [nsA0U sU0U _ _ _] := sdprod_context defU. split; [exists A0 | exists U0]. split=> // [|x Ms_x]; first by rewrite (abelianS (subsetIl A _) cAA). rewrite -(sdprodW defU) -group_modl ?(Frobenius_reg_compl frobM0) ?mulg1 //. by rewrite subIset //= orbC -cent_set1 centS // sub1set; case/setD1P: Ms_x. split=> //; apply/eqP; rewrite eqn_dvd exponentS //=. rewrite -(partnC p (exponent_gt0 U0)) -(partnC p (exponent_gt0 U)). apply: dvdn_mul; last first. rewrite (partn_exponentS sU0U) // -(sdprod_card defU) partnM ?cardG_gt0 //. by rewrite part_p'nat ?pnatNK // mul1n dvdn_part. have cPP: abelian P. have [/(_ P)[] //] := tau2_context maxM t2p Ep2A_M. by apply: subHall_Sylow hallE _ sylP_E; case/andP: t2p. have defP: A0 \x (U0 :&: P) = P. rewrite dprodEsd ?(sub_abelian_cent2 cPP) ?subsetIr //. by rewrite (sdprod_modl defU) // (setIidPr sPU). have sylP_U0: p.-Sylow(U0) (U0 :&: P). rewrite pHallE subsetIl /= -(eqn_pmul2l (cardG_gt0 A0)). rewrite (dprod_card defP) (card_Hall sylP) -(sdprod_card defU). by rewrite partnM // part_pnat_id. rewrite -(exponent_Hall sylP) -(dprod_exponent defP) (exponent_Hall sylP_U0). rewrite dvdn_lcm (dvdn_trans (exponent_dvdn A0)) //= oA0. apply: contraLR piU0p; rewrite -p'natE // -partn_eq1 // partn_part //. by rewrite partn_eq1 ?exponent_gt0 // pnat_exponent -p'groupEpi. have{t2p Ep2A sylS sAS cSS} [[nsE2E cE2E2] hallE2_G _ _] := abelian_tau2 maxM complEi t2p Ep2A sylS sAS cSS. clear p p_pr rU2 piU2p A S Ep2A_M sAE pA cAA. have nsU2U: U2 <| U by rewrite (normalS sU2U sUE) ?normalI. have cU2U2: abelian U2 := abelianS (subsetIl _ _) cE2E2. split. exists U2; rewrite -set1gE; split=> // x /setDP[Ms_x ntx]. rewrite (sub_normal_Hall hallU2) ?subsetIl //=. apply: sub_in_pnat (pgroup_pi _) => q /(piSg (subsetIl U _))/(piSg sUE). rewrite (partition_pi_sigma_compl maxM) // orbCA => /orP[] // t13q. rewrite mem_primes => /and3P[q_pr _ /Cauchy[] // y /setIP[Uy cxy] oy]. case/negP: ntx; rewrite -(regU13 y); first by rewrite inE Ms_x cent1C. by rewrite !inE -order_gt1 oy prime_gt1. by rewrite /p_elt oy pnatE. pose sylU2 S := (S :!=: 1) && Sylow U2 S. pose cyclicRegular Z S := [/\ Z <| U, cyclic Z, 'C_Ms('Ohm_1(Z)) = 1 & exponent Z = exponent S]. suffices /fin_all_exists[Z_ Z_P] S: exists Z, sylU2 S -> cyclicRegular Z S. pose Z2 := <<\bigcup_(S | sylU2 S) Z_ S>>. have sZU2: Z2 \subset U2. rewrite gen_subG; apply/bigcupsP=> S sylS. have [[/andP[sZE _] _ _ eq_expZS] [_ _ sSU2 _]] := (Z_P S sylS, and4P sylS). rewrite (sub_normal_Hall hallU2) // -pnat_exponent eq_expZS. by rewrite pnat_exponent (pgroupS sSU2 t2U2). have nZ2U: U \subset 'N(Z2). by rewrite norms_gen ?norms_bigcup //; apply/bigcapsP => S /Z_P[/andP[]]. have solU: solvable U := solvableS sUE (sigma_compl_sol hallE). have [U31 hallU31] := Hall_exists \tau2(M)^' solU. have [[sU31U t2'U31 _] t2Z2] := (and3P hallU31, pgroupS sZU2 t2U2). pose U0 := (Z2 <*> U31)%G; have /joing_sub[sZ2U0 sU310] := erefl (gval U0). have sU0U: U0 \subset U by rewrite join_subG (subset_trans sZU2). have nsZ2U0: Z2 <| U0 by rewrite /normal sZ2U0 (subset_trans sU0U). have defU0: Z2 * U31 = U0 by rewrite -norm_joinEr // (subset_trans sU31U). have [hallZ2 hallU31_0] := coprime_mulpG_Hall defU0 t2Z2 t2'U31. have expU0U: exponent U0 = exponent U. have exp_t2c U' := partnC \tau2(M) (exponent_gt0 U'). rewrite -(exp_t2c U) -(exponent_Hall hallU31) -(exponent_Hall hallU2). rewrite -{}exp_t2c -(exponent_Hall hallU31_0) -(exponent_Hall hallZ2). congr (_ * _)%N; apply/eqP; rewrite eqn_dvd exponentS //=. apply/dvdn_partP=> [|p]; first exact: exponent_gt0. have [S sylS] := Sylow_exists p U2; rewrite -(exponent_Hall sylS). rewrite pi_of_exponent -p_rank_gt0 -(rank_Sylow sylS) rank_gt0 => ntS. have{} sylS: sylU2 S by rewrite /sylU2 ntS (p_Sylow sylS). by have /Z_P[_ _ _ <-] := sylS; rewrite exponentS ?sub_gen ?(bigcup_max S). exists U0; split=> //. have ntU0: U0 :!=: 1 by rewrite trivg_exponent expU0U -trivg_exponent. apply/Frobenius_semiregularP=> //; first by rewrite (sdprod_subr defMsU). apply: semiregular_sym => x /setD1P[ntx Ms_x]; apply: contraNeq ntx. rewrite -rank_gt0; have [p p_pr ->] := rank_witness [group of 'C_U0[x]]. rewrite -in_set1 -set1gE p_rank_gt0 => piCp. have [e /setIP[U0e cxe] oe]: {e | e \in 'C_U0[x] & #[e] = p}. by move: piCp; rewrite mem_primes p_pr cardG_gt0; apply: Cauchy. have nte: e != 1 by rewrite -order_gt1 oe prime_gt1. have{piCp} piUp: p \in \pi(U). by rewrite -pi_of_exponent -expU0U pi_of_exponent (piSg _ piCp) ?subsetIl. have:= piSg sUE piUp; rewrite (partition_pi_sigma_compl maxM) // orbCA orbC. case/orP=> [t13p | t2p]. rewrite -(regU13 e) 1?inE ?Ms_x 1?cent1C //. by rewrite inE nte (subsetP sU0U). by rewrite /p_elt oe pnatE. have Z2e: e \in Z2 by rewrite (mem_normal_Hall hallZ2) // /p_elt oe pnatE. have [S sylS] := Sylow_exists p U2; have [sSU2 pS _] := and3P sylS. have sylS_U: p.-Sylow(U) S := subHall_Sylow hallU2 t2p sylS. have ntS: S :!=: 1 by rewrite -rank_gt0 (rank_Sylow sylS_U) p_rank_gt0. have sylS_U2: sylU2 S by rewrite /sylU2 ntS (p_Sylow sylS). have [nsZU cycZ regZ1 eqexpZS] := Z_P S sylS_U2. suffices defZ1: 'Ohm_1(Z_ S) == <[e]>. by rewrite -regZ1 (eqP defZ1) cent_cycle inE Ms_x cent1C. have pZ: p.-group (Z_ S) by rewrite -pnat_exponent eqexpZS pnat_exponent. have sylZ: p.-Sylow(Z2) (Z_ S). have:= sZU2; rewrite pHallE /Z2 /= -bigprodGE (bigD1 S) //=. set Z2' := (\prod_(T | _) _)%G => /joing_subP[sZ_U2 sZ2'_U2]. rewrite joing_subl cent_joinEl ?(sub_abelian_cent2 cU2U2) //=. suffices p'Z2': p^'.-group Z2'. rewrite coprime_cardMg ?(pnat_coprime pZ) //. by rewrite partnM // part_pnat_id // part_p'nat // muln1. elim/big_ind: Z2' sZ2'_U2 => [_||T /andP[sylT neqTS]]; first exact: pgroup1. move=> X Y IHX IHY /joing_subP[sXU2 sYU2] /=. by rewrite cent_joinEl ?(sub_abelian_cent2 cU2U2) // pgroupM IHX ?IHY. have /Z_P[_ _ _ expYT _] := sylT. have{sylT} [_ /SylowP[q _ sylT]] := andP sylT. rewrite -pnat_exponent expYT pnat_exponent. apply: (pi_pnat (pHall_pgroup sylT)); apply: contraNneq neqTS => eq_qp. have defOE2 := nilpotent_Hall_pcore (abelian_nil cU2U2). by rewrite -val_eqE /= (defOE2 _ _ sylS) (defOE2 _ _ sylT) eq_qp. have nZZ2 := normalS (pHall_sub sylZ) (subset_trans sZU2 sU2U) nsZU. have Ze: e \in Z_ S by rewrite (mem_normal_Hall sylZ) // /p_elt oe pnat_id. rewrite (eq_subG_cyclic cycZ) ?Ohm_sub ?cycle_subG // -orderE oe. by rewrite (Ohm1_cyclic_pgroup_prime _ pZ) //; apply/trivgPn; exists e. case: (sylU2 S) / andP => [[ntS /SylowP[p p_pr sylS_U2]]|]; last by exists E. have [sSU2 pS _] := and3P sylS_U2; have [sSE2 sSU] := subsetIP sSU2. have piSp: p \in \pi(S) by rewrite -p_rank_gt0 -rank_pgroup ?rank_gt0. have t2p: p \in \tau2(M) := pnatPpi t2U2 (piSg sSU2 piSp). have sylS_U: p.-Sylow(U) S := subHall_Sylow hallU2 t2p sylS_U2. have sylS_E: p.-Sylow(E) S := subHall_Sylow hallU (piSg sSU piSp) sylS_U. have sylS: p.-Sylow(E2) S := pHall_subl sSE2 sE2E sylS_E. have sylS_G: p.-Sylow(G) S := subHall_Sylow hallE2_G t2p sylS. have [cSS [/= s'p rpM]] := (abelianS sSU2 cU2U2, andP t2p). have sylS_M: p.-Sylow(M) S := subHall_Sylow hallE s'p sylS_E. have rpS: 'r_p(S) = 2 by apply/eqP; rewrite (p_rank_Sylow sylS_M). have [A] := p_rank_witness p S; rewrite rpS -(setIidPr (pHall_sub sylS_E)). rewrite pnElemI setIC 2!inE => /andP[sAS Ep2A]. have [[nsAE defEp] _ nregEp_uniq _] := tau2_compl_context maxM hallE t2p Ep2A. have [_ sNS'FE _ sCSE _] := abelian_tau2_sub_Fitting maxM hallE t2p Ep2A sylS_G sAS cSS. have [_ _ [defNS _ _ _] regE1subZ] := abelian_tau2 maxM complEi t2p Ep2A sylS_G sAS cSS. have nSE: E \subset 'N(S) by rewrite -defNS normal_norm. have [sSE nSU] := (subset_trans sSE2 sE2E, subset_trans sUE nSE). have n_subNS := abelian_tau2_norm_Sylow maxM hallE t2p Ep2A sylS_G sAS cSS. have not_sNS_M: ~~ ('N(S) \subset M). by apply: contra s'p => sNS_M; apply/exists_inP; exists S; rewrite // inE. have regNNS Z (Z1 := 'Ohm_1(Z)%G): Z \subset S -> cyclic Z -> Z :!=: 1 -> 'N(S) \subset 'N(Z1) -> 'C_Ms(Z1) = 1. - move=> sZS cycZ ntZ nZ1_NS; apply: contraNeq not_sNS_M => nregZ1. have sZ1S: Z1 \subset S by apply: gFsub_trans. have EpZ1: Z1 \in 'E_p^1(E). rewrite p1ElemE // !inE (subset_trans sZ1S) //=. by rewrite (Ohm1_cyclic_pgroup_prime _ (pgroupS sZS pS)). have /= uCZ1 := nregEp_uniq _ EpZ1 nregZ1. apply: (subset_trans nZ1_NS); apply: (sub_uniq_mmax uCZ1 (cent_sub _)). by rewrite mFT_norm_proper ?(mFT_pgroup_proper (pgroupS sZ1S pS)) ?Ohm1_eq1. have [_ nsCEA t1CEAb] := tau1_cent_tau2Elem_factor maxM hallE t2p Ep2A. have [cSU | not_cSU] := boolP (U \subset 'C(S)). pose n := logn p (exponent S); pose Sn := 'Mho^n.-1(S)%G. have n_gt0: 0 < n by rewrite -pi_of_exponent -logn_gt0 in piSp. have expS: (exponent S = p ^ n.-1 * p)%N. rewrite -expnSr prednK -?p_part //. by rewrite part_pnat_id ?pnat_exponent ?expg_exponent. have sSnS1: Sn \subset 'Ohm_1(S). rewrite (OhmE 1 pS) /= (MhoE _ pS); apply/genS/subsetP=> _ /imsetP[x Sx ->]. by rewrite !inE groupX //= -expgM -expS expg_exponent. have sSZ: S \subset 'Z(U) by rewrite subsetI sSU centsC. have{sSZ} nsZU z: z \in S -> <[z]> <| U. by move=> Sz; rewrite sub_center_normal ?cycle_subG ?(subsetP sSZ). have [homoS | ltSnS1] := eqVproper sSnS1. have Ep2A_M := subsetP (pnElemS p 2 sEM) A Ep2A. have [_ _ _ _ [A1 EpA1 regA1]] := tau2_context maxM t2p Ep2A_M. have [sA1A _ oA1] := pnElemPcard EpA1. have /cyclicP[zn defA1]: cyclic A1 by rewrite prime_cyclic ?oA1. have [z Sz def_zn]: exists2 z, z \in S & zn = z ^+ (p ^ n.-1). apply/imsetP; rewrite -(MhoEabelian _ pS cSS) homoS (OhmE 1 pS). rewrite mem_gen // !inE -cycle_subG -defA1 (subset_trans sA1A) //=. by rewrite -oA1 defA1 expg_order. have oz: #[z] = exponent S. by rewrite expS; apply: orderXpfactor; rewrite // -def_zn orderE -defA1. exists <[z]>%G; split; rewrite ?cycle_cyclic ?exponent_cycle ?nsZU //. by rewrite (Ohm_p_cycle _ (mem_p_elt pS Sz)) subn1 oz -def_zn -defA1. have [z Sz /esym oz] := exponent_witness (abelian_nil cSS). exists <[z]>%G; split; rewrite ?cycle_cyclic ?exponent_cycle ?nsZU //. have ntz: <[z]> != 1 by rewrite trivg_card1 -orderE oz -dvdn1 -trivg_exponent. rewrite regNNS ?cycle_cyclic ?cycle_subG //=. suffices /eqP->: 'Ohm_1(<[z]>) == Sn by apply: char_norms; apply: gFchar. have [p_z pS1] := (mem_p_elt pS Sz, pgroupS (Ohm_sub 1 S) pS). rewrite eqEcard (Ohm1_cyclic_pgroup_prime _ p_z) ?cycle_cyclic //. rewrite (Ohm_p_cycle _ p_z) oz -/n subn1 cycle_subG Mho_p_elt //=. rewrite (card_pgroup (pgroupS sSnS1 pS1)) (leq_exp2l _ 1) ?prime_gt1 //. by rewrite -ltnS -rpS p_rank_abelian ?properG_ltn_log. have{not_cSU} [q q_pr piUq]: {q | prime q & q \in \pi(U / 'C(S))}. have [q q_pr rCE] := rank_witness (U / 'C(S)); exists q => //. by rewrite -p_rank_gt0 -rCE rank_gt0 -subG1 quotient_sub1 ?norms_cent. have{piUq} [piCESbq piUq]: q \in \pi(E / 'C_E(S)) /\ q \in \pi(U). rewrite /= setIC (card_isog (second_isog (norms_cent nSE))). by rewrite (piSg _ piUq) ?quotientS // (pi_of_dvd _ _ piUq) ?dvdn_quotient. have [Q1 sylQ1_U] := Sylow_exists q U; have [sQ1U qQ1 _] := and3P sylQ1_U. have sylQ1: q.-Sylow(E) Q1 := subHall_Sylow hallU piUq sylQ1_U. have sQ1E := subset_trans sQ1U sUE; have nSQ1 := subset_trans sQ1E nSE. have [Q sylQ sQ1Q] := Sylow_superset nSQ1 qQ1; have [nSQ qQ _] := and3P sylQ. have Ep2A_M := subsetP (pnElemS p 2 sEM) A Ep2A. have ltCQ1_S: 'C_S(Q1) \proper S. rewrite properE subsetIl /= subsetI subxx centsC -sQ1E -subsetI. have nCES_Q1: Q1 \subset 'N('C_E(S)) by rewrite (setIidPr sCSE) norms_cent. rewrite -quotient_sub1 // subG1 -rank_gt0. by rewrite (rank_Sylow (quotient_pHall nCES_Q1 sylQ1)) p_rank_gt0. have coSQ: coprime #|S| #|Q|. suffices p'q: q != p by rewrite (pnat_coprime pS) // (pi_pnat qQ). apply: contraNneq (proper_subn ltCQ1_S) => eq_qp; rewrite subsetI subxx. rewrite (sub_abelian_cent2 cE2E2) // (sub_normal_Hall hallE2) //. by rewrite (pi_pgroup qQ1) ?eq_qp. have not_sQ1CEA: ~~ (Q1 \subset 'C_E(A)). rewrite subsetI sQ1E; apply: contra (proper_subn ltCQ1_S) => /= cAQ1. rewrite subsetIidl centsC coprime_abelian_faithful_Ohm1 ?(coprimegS sQ1Q) //. by case: (tau2_context maxM t2p Ep2A_M); case/(_ S sylS_M)=> _ [|->] //. have t1q: q \in \tau1(M). rewrite (pnatPpi t1CEAb) // -p_rank_gt0. have nCEA_Q1: Q1 \subset 'N('C_E(A)) := subset_trans sQ1E (normal_norm nsCEA). rewrite -(rank_Sylow (quotient_pHall nCEA_Q1 sylQ1)) rank_gt0. by rewrite -subG1 quotient_sub1. have cycQ1: cyclic Q1. have [x _ sQ1E1x] := Hall_psubJ hallE1 t1q sQ1E qQ1. by rewrite (cyclicS sQ1E1x) ?cyclicJ. have defQ1: Q :&: E = Q1. apply: (sub_pHall sylQ1) (subsetIr Q E); last by rewrite subsetI sQ1Q. by rewrite (pgroupS (subsetIl Q _)). pose Q0 := 'C_Q(S); have nsQ0Q: Q0 <| Q by rewrite norm_normalI ?norms_cent. have [sQ0Q nQ0Q] := andP nsQ0Q; have nQ01 := subset_trans sQ1Q nQ0Q. have coSQ0: coprime #|S| #|Q0| := coprimegS sQ0Q coSQ. have ltQ01: Q0 \proper Q1. rewrite /proper -{1}defQ1 setIS //. apply: contra (proper_subn ltCQ1_S) => sQ10. by rewrite subsetIidl (centsS sQ10) // centsC subsetIr. have [X]: exists2 X, X \in subgroups Q & ('C_S(X) != 1) && ([~: S, X] != 1). apply/exists_inP; apply: contraFT (ltnn 1); rewrite negb_exists_in => irrS. have [sQ01 not_sQ10] := andP ltQ01. have qQb: q.-group (Q / Q0) by apply: quotient_pgroup. have ntQ1b: Q1 / Q0 != 1 by rewrite -subG1 quotient_sub1. have ntQb: Q / Q0 != 1 := subG1_contra (quotientS _ sQ1Q) ntQ1b. have{irrS} regQ: semiregular (S / Q0) (Q / Q0). move=> Q0x; rewrite 2!inE -cycle_subG -cycle_eq1 -cent_cycle andbC. case/andP; case/(inv_quotientS nsQ0Q)=> X /= -> {Q0x} sQ0X sXQ ntXb. have [nSX nQ0X] := (subset_trans sXQ nSQ, subset_trans sXQ nQ0Q). rewrite -quotient_TI_subcent ?(coprime_TIg coSQ0) //. apply: contraTeq (forallP irrS X) => ntCSXb; rewrite inE sXQ negbK. apply/andP; split. by apply: contraNneq ntCSXb => ->; rewrite quotient1. apply: contraNneq ntXb; move/commG1P => cXS. by rewrite quotientS1 // subsetI sXQ centsC. have{regQ} cycQb: cyclic (Q / Q0). have nSQb: Q / Q0 \subset 'N(S / Q0) by apply: quotient_norms. apply: odd_regular_pgroup_cyclic qQb (mFT_quo_odd _ _) _ nSQb regQ. rewrite -(isog_eq1 (quotient_isog _ _)) ?coprime_TIg 1?coprime_sym //. by rewrite cents_norm // centsC subsetIr. have rQ1: 'r(Q1) = 1%N. apply/eqP; rewrite (rank_Sylow sylQ1). by rewrite (tau1E maxM hallE) in t1q; case/and3P: t1q. have: 'r(Q) <= 1; last apply: leq_trans. have nQ0_Ohm1Q: 'Ohm_1(Q) \subset 'N(Q0) by apply: gFsub_trans. rewrite -rQ1 -rank_Ohm1 rankS // -(quotientSGK _ sQ01) //. rewrite (subset_trans (morphim_Ohm _ _ nQ0Q)) //= -quotientE -/Q0. rewrite -(cardSg_cyclic cycQb) ?Ohm_sub ?quotientS //. have [_ q_dv_Q1b _] := pgroup_pdiv (pgroupS (quotientS _ sQ1Q) qQb) ntQ1b. by rewrite (Ohm1_cyclic_pgroup_prime cycQb qQb ntQb). have ltNA_G: 'N(A) \proper G. by rewrite defNS mFT_norm_proper // (mFT_pgroup_proper pS). have [H maxNA_H] := mmax_exists ltNA_G. have nCEA_Q1 := subset_trans sQ1E (normal_norm nsCEA). have [_ _] := primes_norm_tau2Elem maxM hallE t2p Ep2A maxNA_H. case/(_ q)=> [||t2Hq [S2 sylS2 nsS2H] _]. - rewrite -p_rank_gt0 -(rank_Sylow (quotient_pHall _ sylQ1)) //. by rewrite rank_gt0 -subG1 quotient_sub1. - rewrite -p_rank_gt0 -rQ1 (rank_pgroup qQ1) -p_rank_Ohm1 p_rankS //. have: 'Z(E) \subset 'C_E(A); last apply: subset_trans. by rewrite setIS ?centS // normal_sub. have [x Ex sQ1xE1] := Hall_pJsub hallE1 t1q sQ1E qQ1. rewrite -(conjSg _ _ x) ['Z(E) :^ x](normsP _ x Ex) ?gFnorm //. set Q11x := _ :^ x; have oQ11x: #|Q11x| = q. by rewrite cardJg (Ohm1_cyclic_pgroup_prime _ qQ1) // -rank_gt0 rQ1. apply: regE1subZ; rewrite /= -/Q11x. apply/nElemP; exists q; rewrite p1ElemE // !inE oQ11x. by rewrite (subset_trans _ sQ1xE1) //= conjSg Ohm_sub. have /cyclicP[y defQ11x]: cyclic Q11x by rewrite prime_cyclic ?oQ11x. rewrite defQ11x cent_cycle regU13 //. rewrite !inE -order_gt1 -cycle_subG /order -defQ11x oQ11x prime_gt1 //. by rewrite -(normsP (normal_norm nsUE) x Ex) conjSg gFsub_trans. by rewrite /p_elt /order -defQ11x oQ11x pnatE //; apply/orP; left. rewrite inE in sylS2; have [sS2H _]:= andP nsS2H. have sylS2_H := pHall_subl sS2H (subsetT H) sylS2. have [maxH sNS_H] := setIdP maxNA_H; rewrite /= defNS in sNS_H. have sylS_H := pHall_subl (subset_trans (normG S) sNS_H) (subsetT H) sylS_G. have defS2: S :=: S2 := uniq_normal_Hall sylS2_H nsS2H (Hall_max sylS_H). have sylQ_H: q.-Sylow(H) Q by rewrite -(mmax_normal maxH nsS2H) -defS2. by rewrite (rank_Sylow sylQ_H); case/andP: t2Hq => _ /eqP->. rewrite inE => sXQ /=; have nSX := subset_trans sXQ nSQ. set S1 := [~: S, X]; set S2 := 'C_S(X) => /andP[ntS2 ntS1]. have defS12: S1 \x S2 = S. by apply: coprime_abelian_cent_dprod; rewrite ?(coprimegS sXQ). have /mulG_sub[sS1S sS2S] := dprodW defS12. have [cycS1 cycS2]: cyclic S1 /\ cyclic S2. apply/andP; rewrite !(abelian_rank1_cyclic (abelianS _ cSS)) //. rewrite -(leqif_add (leqif_geq _) (leqif_geq _)) ?rank_gt0 // addn1 -rpS. rewrite !(rank_pgroup (pgroupS _ pS)) ?(p_rank_abelian p (abelianS _ cSS)) //. by rewrite -lognM ?cardG_gt0 // (dprod_card (Ohm_dprod 1 defS12)). have [nsS2NS nsS1NS]: S2 <| 'N(S) /\ S1 <| 'N(S) := n_subNS X nSX. pose Z := if #|S1| < #|S2| then [group of S2] else [group of S1]. have [ntZ sZS nsZN cycZ]: [/\ Z :!=: 1, Z \subset S, Z <| 'N(S) & cyclic Z]. by rewrite /Z; case: ifP. have nsZU: Z <| U := normalS (subset_trans sZS sSU) nSU nsZN. exists Z; split=> //=. by rewrite regNNS // (char_norm_trans (Ohm_char 1 Z)) // normal_norm. rewrite -(dprod_exponent defS12) /= (fun_if val) fun_if !exponent_cyclic //=. rewrite (card_pgroup (pgroupS sS1S pS)) (card_pgroup (pgroupS sS2S pS)) //. by rewrite /= -/S1 -/S2 ltn_exp2l ?prime_gt1 // -fun_if expn_max. 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)