proposition: Theorem BGsummaryC : K :!=: 1 -> [/\ [/\ abelian U /\ ~~ ('N(U) \subset M), [/\ cyclic Kstar, Kstar != 1, Kstar \subset M`_\F & ~~ cyclic M`_\F] & M`_\sigma ><| U = M^`(1) /\ Kstar \subset M^`(2)], exists Mstar, [/\ [/\ Mstar \in 'M_'P, 'C_(Mstar`_\sigma)(Kstar) = K, \kappa(Mstar).-Hall(Mstar) Kstar & 'M_\sigma(K) = [set Mstar]], {in 'E^1(Kstar), forall X, 'M('C(X)) = [set M]} /\ {in 'E^1(K), forall Y, 'M('C(Y)) = [set Mstar]}, [/\ M :&: Mstar = Z, K \x Kstar = Z & cyclic Z] & (M \in 'M_'P2 \/ Mstar \in 'M_'P2) /\ {in 'M_'P, forall H, gval H \in M :^: G :|: Mstar :^: G}] & [/\ normedTI Zhat G Z, let B := 'A0(M) :\: 'A(M) in B = class_support Zhat M /\ normedTI B G M, U :!=: 1 -> [/\ prime #|K|, normedTI 'F(M)^# G M & M`_\sigma \subset 'F(M)] & U :==: 1 -> prime #|Kstar| ]].
proof: Proof. move=> ntK; have [_ hallK _] := complU. have PmaxM: M \in 'M_'P by rewrite inE -(trivg_kappa maxM hallK) ntK. split. - have [_ [//|-> ->] _ _ _] := kappa_structure maxM complU. have [-> -> -> -> ->] := Ptype_cyclics PmaxM hallK; do 2!split=> //. have [L maxCK_L] := mmax_exists (mFT_cent_proper ntK). have [-> | ntU] := eqsVneq U 1. by rewrite norm1 proper_subn // mmax_proper. have P2maxM: M \in 'M_'P2 by rewrite inE -(trivg_kappa_compl maxM complU) ntU. have [r _ rU] := rank_witness U; have [R sylR] := Sylow_exists r U. have ntR: R :!=: 1 by rewrite -rank_gt0 (rank_Sylow sylR) -rU rank_gt0. have ltRG: R \proper G := mFT_pgroup_proper (pHall_pgroup sylR). have [H maxNR_H] := mmax_exists (mFT_norm_proper ntR ltRG). apply: contra (subset_trans (subsetIr H _)) _. by have [_ _ _ [->]] := P2type_signalizer P2maxM complU maxCK_L sylR maxNR_H. - have [L [PmaxL _] [uniqL []]] := Ptype_embedding PmaxM hallK. rewrite -/Kstar -/Z -/Zhat => hallKstar _ [defK _] [cycZ defML _ _ _]. case=> _ P2_MorL Pmax_conjMorL _; exists L. suffices uniqMSK: 'M_\sigma(K) = [set L]. have [_ [defNK _] [_ uniqM] _ _] := Ptype_structure PmaxM hallK. do 2!split=> //; last by case: P2_MorL => [] [-> _]; [left | right]. by have [_ _ cKKs tiKKs] := dprodP defNK; rewrite dprodEY. have sKLs: K \subset L`_\sigma by rewrite -defK subsetIl. have [X E1X]: exists X, X \in 'E^1(K) by apply/rank_geP; rewrite rank_gt0. have sXK: X \subset K by case/nElemP: E1X => ? /pnElemP[]. have [maxL sCXL] := mem_uniq_mmax (uniqL X E1X). have [x defKx] := cyclicP (cyclicS (joing_subl _ _) cycZ). have SMxL: L \in 'M_\sigma[x] by rewrite -defKx inE maxL. have ell1x: \ell_\sigma(x) == 1%N. by rewrite (Msigma_ell1 maxL) // !inE -cycle_eq1 -cycle_subG -defKx ntK. apply/eqP; rewrite eq_sym eqEcard defKx sub1set SMxL cards1 leqNgt. apply/negP=> ntSMx; have [_ [//|_ ntR _ _]] := FT_signalizer_context ell1x. case/(_ L)=> // /sdprodP[_ _ _ tiRL]; case/negP: ntR. rewrite -subG1 -tiRL subsetIidl -setIA setICA setISS ?pcore_sub //. by rewrite subsetIidr /= -cent_cycle -defKx (subset_trans (centS sXK) sCXL). split; last 1 first. - rewrite (trivg_kappa_compl maxM complU) => P1maxM. have [L _ [_ _ _ _ [_ [] [] //]]] := Ptype_embedding PmaxM hallK. by rewrite inE P1maxM. - by have [L _ [_ _ _ _ [[]]]] := Ptype_embedding PmaxM hallK. - have [L _ [_ _ _]] := Ptype_embedding PmaxM hallK; rewrite -/Zhat -/Z. case=> cycZ defML defCK defCKs defCZhat [[tiZhat tiZhatM _] _ _ defM] B. have sZM: Z \subset M by rewrite -[Z]defML subsetIl. have sZhM: Zhat \subset M by rewrite subDset setUC subsetU ?sZM. suffices defB: B = class_support Zhat M. split=> //; apply/normedTI_P. rewrite setTI normsD ?FTsupp_norm ?FTsupp0_norm //; split=> // [|g _]. case/andP: tiZhat => /set0Pn[z Zz] _; apply/set0Pn; exists z. by rewrite defB mem_class_support. rewrite defB => /pred0Pn[_ /andP[/imset2P[z x Zz Mx ->] /= Bg_zx]]. apply/idPn; rewrite -(groupMr g (groupVr Mx)) -in_setC. case/tiZhatM/pred0Pn; exists z; rewrite /= Zz conjsgM mem_conjgV. by apply: subsetP Bg_zx; rewrite conjSg class_support_subG. rewrite /B /'A0(M); set M' := M^`(_); set su := \pi(M'). have defM': M' = M^`(1) by rewrite /M' -FTtype_Pmax ?PmaxM. have{hallK} hallM': su.-Hall(M) M'. by rewrite Hall_pi //= -/M' defM' (sdprod_Hall defM) (pHall_Hall hallK). have{hallM'} hallK: su^'.-Hall(M) K. by rewrite -(compl_pHall _ hallM') /= -/M' defM' sdprod_compl. have su'K: su^'.-group K := pHall_pgroup hallK. have suKs: su.-group Kstar. by rewrite (pgroupS _ (pgroup_pi _)) ///= -/M' defM' subIset ?Msigma_der1. apply/setP=> x; rewrite !inE; apply/andP/imset2P=> [[]| [y a]]; last first. case/setDP=> Zy; rewrite inE => /norP[not_Ky notKs_y] Ma ->. have My := subsetP sZM y Zy; have Mya := groupJ My Ma. have [not_suy not_su'y]: ~~ su.-elt y /\ ~~ su^'.-elt y. have defZ: K * Kstar = Z by rewrite -cent_joinEr ?subsetIr. have [hallK_Z hallKs] := coprime_mulGp_Hall defZ su'K suKs. have ns_Z := sub_abelian_normal _ (cyclic_abelian cycZ). rewrite -(mem_normal_Hall hallKs) -?ns_Z ?joing_subr // notKs_y. by rewrite -(mem_normal_Hall hallK_Z) -?ns_Z ?joing_subl. rewrite Mya !p_eltJ not_suy not_su'y orbT; split=> //. apply: contra not_suy => /bigcupP[_ _ /setD1P[_ /setIP[M'ya _]]]. by rewrite -(p_eltJ _ y a) (mem_p_elt (pgroup_pi _)). move/negPf=> -> /and3P[Mx not_sux not_su'x]; set y := x.`_su^'. have syM: <[y]> \subset M by rewrite cycle_subG groupX. have [a Ma Kya] := Hall_Jsub (mmax_sol maxM) hallK syM (p_elt_constt _ _). have{Kya} K1ya: y ^ a \in K^#. rewrite !inE -cycle_subG cycleJ Kya andbT -consttJ. by apply: contraNneq not_sux; move/constt1P; rewrite p_eltNK p_eltJ. exists (x ^ a) a^-1; rewrite ?groupV ?conjgK // 2!inE andbC negb_or. rewrite -[Z](defCK _ K1ya) inE groupJ // cent1C -consttJ groupX ?cent1id //. by rewrite (contra (mem_p_elt su'K)) ?(contra (mem_p_elt suKs)) ?p_eltJ. rewrite (trivg_kappa_compl maxM complU) => notP1maxM. have P2maxM: M \in 'M_'P2 by apply/setDP. split; first by have [_ _ _ _ []] := Ptype_structure PmaxM hallK. apply: contraR notP1maxM; case/nonTI_Fitting_facts=> //. by case/setUP=> //; case/idPn; case/setDP: PmaxM. have [<- | neqMF_Ms] := eqVneq M`_\F M`_\sigma; first exact: Fcore_sub_Fitting. have solMs: solvable M`_\sigma := solvableS (pcore_sub _ _) (mmax_sol maxM). have [D hallD] := Hall_exists #|Kstar|^' solMs. by case: (Fcore_structure maxM) notP1maxM => _ /(_ K D)[] // [->]. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div path fintype) mathcomp(bigop finset prime fingroup morphism perm automorphism quotient) mathcomp(action gproduct gfunctor pgroup cyclic center commutator) mathcomp(gseries nilpotent sylow abelian maximal hall frobenius) odd_order(BGsection1 BGsection2 BGsection3 BGsection4 BGsection5) odd_order(BGsection6 BGsection7 BGsection9 BGsection10 BGsection12) odd_order(BGsection13 BGsection14 BGsection15)