proposition: Theorem BGsummaryB : [/\ forall p S, p.-Sylow(U) S -> abelian S /\ 'r(S) <= 2, abelian <<U :&: 'A(M)>>, exists U0 : {group gT}, [/\ U0 \subset U, exponent U0 = exponent U & [disjoint U0 & 'A(M)]] & (forall X, X \subset U -> X :!=: 1 -> 'C_(M`_\sigma)(X) != 1 -> 'M('C(X)) = [set M]) /\ ('A(M) != 'A1(M) -> normedTI ('A(M) :\: 'A1(M)) G M)].
proof: Proof. split. - move=> p S sylS; have [hallU _ _] := complU; have [sUM sk'U _] := and3P hallU. have [-> | ntS] := eqsVneq S 1; first by rewrite abelian1 rank1. have sk'p: p \in \sigma_kappa(M)^'. by rewrite (pnatPpi sk'U) // -p_rank_gt0 -(rank_Sylow sylS) rank_gt0. have{} sylS := subHall_Sylow hallU sk'p sylS. have [[sSM pS _] [/= s'p _]] := (and3P sylS, norP sk'p). rewrite (sigma'_nil_abelian maxM) ?(pi_pgroup pS) ?(pgroup_nil pS) //. by rewrite (rank_Sylow sylS) leqNgt (contra _ s'p) //; apply: alpha_sub_sigma. - have [_ _ _ cUA_UA _] := kappa_structure maxM complU. apply: abelianS cUA_UA; rewrite genS // -big_distrr ?setIS -?def_FTcore //=. by apply/bigcupsP=> x A1x; rewrite (bigcup_max x) // setDE setIAC subsetIr. - have [-> | ntU] := eqsVneq U 1. exists 1%G; split; rewrite // disjoint_sym disjoints_subset. by apply/bigcupsP=> x _; rewrite setDE subsetIr. have [_ _ _ _ [// | U0 [sU0U expU0 frobU0]]] := kappa_structure maxM complU. exists U0; split; rewrite // -setI_eq0 big_distrr /= /'A1(M) def_FTcore //. rewrite big1 // => x A1x; apply/eqP; rewrite setIDA setD_eq0 setICA. by rewrite (Frobenius_reg_compl frobU0) ?subsetIr. set part4 := forall X, _; have part4holds: part4. move=> X sXU ntX nregX. by have [_ _] := kappa_structure maxM complU; case/(_ X). have [[nsMsM _ _] _ [_ _ nsMsUM _ _] _ _] := BGsummaryA. have{nsMsM nsMsUM}[[_ nMsM] [_ nMsUM]] := (andP nsMsM, andP nsMsUM). rewrite eqEsubset FTsupp1_sub // -setD_eq0 andbT; set B := _ :\: _. have nBM: M \subset 'N(B) by rewrite normsD ?FTsupp_norm ?FTsupp1_norm. have uniqB y (u := y.`_\sigma(M)^'): y \in B -> 'M('C[u]) = [set M]. case/setDP=> /bigcupP[x /setD1P[ntx Ms_x] /setD1P[nty /setIP[M'y cxy]]]. rewrite !inE nty def_FTcore //= in Ms_x * => notMs_y; set M' := M^`(_) in M'y. have [nsMsM' _ _ _ _] := sdprod_context sdprod_FTder. have [[sMsM' nMsM'] sM'M]:= (andP nsMsM', der_sub _ M : M' \subset M). have hallMs := pHall_subl sMsM' sM'M (Msigma_Hall maxM). have hallU: \sigma(M)^'.-Hall(M') U. by rewrite -(compl_pHall _ hallMs) sdprod_compl ?sdprod_FTder. have suM': <[u]> \subset M' by rewrite cycle_subG groupX. have solM': solvable M' := solvableS sM'M (mmax_sol maxM). have [z M'z suzU] := Hall_Jsub solM' hallU suM' (p_elt_constt _ _). have Mz': z^-1 \in M by rewrite groupV (subsetP sM'M). rewrite -(conjgK z u) -(group_inj (conjGid Mz')) -cent_cycle. rewrite !cycleJ centJ; apply: def_uniq_mmaxJ (part4holds _ suzU _ _). rewrite /= -cycleJ cycle_eq1 -consttJ; apply: contraNneq notMs_y. move/constt1P; rewrite p_eltNK p_eltJ => sMy. by rewrite (mem_normal_Hall hallMs). rewrite -(normsP nMsM' z M'z) centJ -conjIg -(isog_eq1 (conj_isog _ _)). by apply/trivgPn; exists x; rewrite //= inE Ms_x cent_cycle cent1C groupX. split=> // nzB; apply/normedTI_P; rewrite setTI; split=> // a _. case/pred0Pn=> x /andP[/= Bx]; rewrite mem_conjg => /uniqB/(def_uniq_mmaxJ a). rewrite consttJ -normJ conjg_set1 conjgKV uniqB // => /set1_inj defM. by rewrite -(norm_mmax maxM) inE {2}defM. 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)