proposition: Lemma exceptional_TIsigmaJ g q Q1 Q2 : g \notin M -> A \subset M :^ g -> q.-Sylow(M`_\sigma) Q1 -> A \subset 'N(Q1) -> q.-Sylow(M`_\sigma :^ g) Q2 -> A \subset 'N(Q2) -> Q1 :&: Q2 = 1 /\ (forall X, X \in 'E_p^1(A) -> 'C_Q1(X) = 1 \/ 'C_Q2(X) = 1).
proof: Proof. move=> notMg sAMg sylQ1 nQ1A sylQ2 nQ2A. have [-> | ntQ1] := eqsVneq Q1 1. by split=> [|? _]; last left; apply: (setIidPl (sub1G _)). have [sQ1Ms qQ1 _] := and3P sylQ1. have{qQ1} [q_pr q_dv_Q1 _] := pgroup_pdiv qQ1 ntQ1. have{sQ1Ms q_dv_Q1} sMq: q \in \sigma(M). exact: pgroupP (pgroupS sQ1Ms (pcore_pgroup _ _)) q q_pr q_dv_Q1. have{} sylQ1: q.-Sylow(M) Q1. by rewrite (subHall_Sylow (Msigma_Hall maxM)). have sQ1M := pHall_sub sylQ1. have{sylQ2} sylQ2g': q.-Sylow(M) (Q2 :^ g^-1). by rewrite (subHall_Sylow (Msigma_Hall _)) // -(pHallJ2 _ _ _ g) actKV. have sylQ2: q.-Sylow(G) Q2. by rewrite -(pHallJ _ _ (in_setT g^-1)) (sigma_Sylow_G maxM). suffices not_Q1_CA_Q2: gval Q2 \notin Q1 :^: 'O_\pi(A)^'('C(A)). have ncA: normed_constrained A. have ntA: A :!=: 1 by rewrite -cardG_gt1 oA (ltn_exp2l 0). exact: plength_1_normed_constrained ntA EpmA (mFT_proper_plength1 _). have q'A: q \notin \pi(A). by apply: contraL sMq; move/(pnatPpi pA); move/eqnP->. have maxnAq Q: q.-Sylow(G) Q -> A \subset 'N(Q) -> Q \in |/|*(A; q). move=> sylQ; case/(max_normed_exists (pHall_pgroup sylQ)) => R maxR sQR. have [qR _] := mem_max_normed maxR. by rewrite -(group_inj (sub_pHall sylQ qR sQR (subsetT R))). have maxQ1 := maxnAq Q1 (sigma_Sylow_G maxM sMq sylQ1) nQ1A. have maxQ2 := maxnAq Q2 sylQ2 nQ2A. have transCAQ := normed_constrained_meet_trans ncA q'A _ _ maxQ1 maxQ2. split=> [|X EpX]. apply: contraNeq not_Q1_CA_Q2 => ntQ12; apply/imsetP. apply: transCAQ (sAM) (mmax_proper maxM) _ _. by rewrite (setIidPl sQ1M). by apply: contraNneq ntQ12 => tiQ2M; rewrite setIC -subG1 -tiQ2M setIS. apply/pred2P; apply: contraR not_Q1_CA_Q2; case/norP=> ntCQ1 ntCQ2. have [sXA _ oX] := pnElemPcard EpX. apply/imsetP; apply: transCAQ (centSS _ sXA cAA) _ ntCQ1 ntCQ2 => //. by rewrite mFT_cent_proper // -cardG_gt1 oX prime_gt1. apply: contra notMg; case/imsetP=> k cAk defQ2. have{cAk} Mk := subsetP sCA_M k (subsetP (pcore_sub _ _) k cAk). have{k Mk defQ2} sQ2M: Q2 \subset M by rewrite defQ2 conj_subG. have [sQ2g'M qQ2g' _] := and3P sylQ2g'. by rewrite (sigma_Sylow_trans _ sylQ2g') // actKV. 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)