proposition: Corollary exceptional_TI_MsigmaJ g : g \notin M -> A \subset M :^ g -> M`_\sigma :&: M :^ g = 1 /\ M`_\sigma :&: 'C(A0 :^ g) = 1.
proof: Proof. move=> notMg sAMg; set Ms := M`_\sigma; set H := [group of Ms :&: M :^ g]. have [H1 | ntH] := eqsVneq H 1. by split=> //; apply/trivgP; rewrite -H1 setIS //= centJ conjSg. pose q := pdiv #|H|. suffices: #|H|`_q == 1%N by rewrite p_part_eq1 pi_pdiv cardG_gt1 ntH. have nsMsM: Ms <| M := pcore_normal _ _; have [_ nMsM] := andP nsMsM. have sHMs: H \subset Ms := subsetIl _ _. have sHMsg: H \subset Ms :^ g. rewrite -sub_conjgV (sub_Hall_pcore (Msigma_Hall _)) //. by rewrite pgroupJ (pgroupS sHMs) ?pcore_pgroup. by rewrite sub_conjgV subsetIr. have nMsA := subset_trans sAM nMsM. have nHA: A \subset 'N(H) by rewrite normsI // normsG. have nMsgA: A \subset 'N(Ms :^ g) by rewrite normJ (subset_trans sAMg) ?conjSg. have coMsA: coprime #|Ms| #|A|. by rewrite oA coprimeXr ?(pnat_coprime (pcore_pgroup _ _)) ?pnatE. have coHA: coprime #|H| #|A| := coprimeSg sHMs coMsA. have coMsgA: coprime #|Ms :^ g| #|A| by rewrite cardJg. have solA: solvable A := abelian_sol cAA. have [Q0 sylQ0 nQ0A] := sol_coprime_Sylow_exists q solA nHA coHA. have [sQ0H qQ0 _] := and3P sylQ0. have supQ0 := sol_coprime_Sylow_subset _ _ solA (subset_trans sQ0H _) qQ0 nQ0A. have [Q1 [sylQ1 nQ1A sQ01]] := supQ0 _ nMsA coMsA sHMs. have [Q2 [sylQ2 nQ2A sQ02]] := supQ0 _ nMsgA coMsgA sHMsg. have tiQ12: Q1 :&: Q2 = 1. by have [-> _] := exceptional_TIsigmaJ notMg sAMg sylQ1 nQ1A sylQ2 nQ2A. by rewrite -(card_Hall sylQ0) -trivg_card1 -subG1 -tiQ12 subsetI sQ01. 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) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection10)