proposition: Theorem BGsummaryA : [/\ [/\ M`_\sigma <| M, \sigma(M).-Hall(M) M`_\sigma & \sigma(M).-Hall(G) M`_\sigma], \kappa(M).-Hall(M) K /\ cyclic K, [/\ U \in [complements to M`_\sigma <*> K in M], K \subset 'N(U), M`_\sigma <*> U <| M, U <| U <*> K & M`_\sigma * U * K = M], {in K^#, forall k, 'C_U[k] = 1} & [/\ Kstar != 1 /\ {in K^#, forall k, K \x Kstar = 'C_M[k]}, [/\ M`_\F != 1, M`_\F \subset M`_\sigma, M`_\sigma \subset M^`(1), M^`(1) \proper M & nilpotent (M^`(1) / M`_\F)], [/\ M^`(2) \subset 'F(M), M`_\F * 'C_M(M`_\F) = 'F(M) & K :!=: 1 -> 'F(M) \subset M^`(1)] & M`_\F != M`_\sigma -> [/\ U :=: 1, normedTI 'F(M)^# G M & prime #|K| ]]].
proof: Proof. have [hallU hallK _] := complU; split. - by rewrite pcore_normal Msigma_Hall // Msigma_Hall_G. - by have [[]] := kappa_structure maxM complU. - have [_ defM _ _ _] := kappa_compl_context maxM complU. have [[_ UK _ defUK]] := sdprodP defM; rewrite defUK. have [nsKUK _ mulUK nUK _] := sdprod_context defUK. rewrite -mulUK mulG_subG mulgA => mulMsUK /andP[nMsU nMsK] _. rewrite (norm_joinEr nUK) mulUK; split=> //. rewrite inE coprime_TIg /= norm_joinEr //=. by rewrite -mulgA (normC nUK) mulgA mulMsUK !eqxx. rewrite (pnat_coprime _ (pHall_pgroup hallU)) // -pgroupE pgroupM. rewrite (sub_pgroup _ (pHall_pgroup hallK)) => [|p k_p]; last first. by apply/orP; right. by rewrite (sub_pgroup _ (pcore_pgroup _ _)) => // p s_p; apply/orP; left. have{defM} [[defM _ _] _ _ _ _] := kappa_structure maxM complU. have [[MsU _ defMsU] _ _ _ _] := sdprodP defM; rewrite defMsU in defM. have [_ mulMsU _ _] := sdprodP defMsU. by rewrite norm_joinEr // mulMsU; case/sdprod_context: defM. - by have [] := kappa_compl_context maxM complU. split. - have [K1 | ntK] := eqsVneq K 1. rewrite /Kstar K1 cent1T setIT Msigma_neq1 // setDv. by split=> // k; rewrite inE. have PmaxM: M \in 'M_'P by rewrite inE -(trivg_kappa maxM hallK) ntK. have [_ [defNK _] [-> _] _ _] := Ptype_structure PmaxM hallK. have [_ _ cKKs tiKKs] := dprodP defNK; rewrite dprodEY //; split=> // k Kk. by have [_ _ [_ _ _ [_ _ -> // _ _] _]] := Ptype_embedding PmaxM hallK. - have [_ _ [_ ->] _] := Fitting_structure maxM. by have [[]] := Fcore_structure maxM. - have [_ [-> defF _] _ sFM'] := Fitting_structure maxM. have [_ -> _] := cprodP defF; split=> // ntK. by rewrite sFM' // inE -(trivg_kappa maxM hallK) ntK. move=> not_nilMs; pose q := #|Kstar|. have solMs: solvable M`_\sigma := solvableS (pcore_sub _ _) (mmax_sol maxM). have [D hallD] := Hall_exists q^' solMs. have [_] := Fcore_structure maxM; case/(_ K D)=> //. case=> P1maxM _ _ [-> _ _ _] _ _ _; split=> //. by apply/eqP; rewrite (trivg_kappa_compl maxM complU). by apply: contraR not_nilMs; case/nonTI_Fitting_facts=> // _ -> _. 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)