proposition: Lemma sigma_disjoint M H : M \in 'M -> H \in 'M -> gval H \notin M :^: G -> [/\ M`_\alpha :&: H`_\sigma = 1, [predI \alpha(M) & \sigma(H)] =i pred0 & nilpotent M`_\sigma -> M`_\sigma :&: H`_\sigma = 1 /\ [predI \sigma(M) & \sigma(H)] =i pred0].
proof: Proof. move=> maxM maxH notjMH. suffices sigmaMHnil p: p \in [predI \sigma(M) & \sigma(H)] -> p \notin \alpha(M) /\ ~~ nilpotent M`_\sigma. - have a2: [predI \alpha(M) & \sigma(H)] =i pred0. move=> p; apply/andP=> [[/= aMp sHp]]. by case: (sigmaMHnil p); rewrite /= ?aMp // inE /= alpha_sub_sigma. split=> // [|nilMs]. rewrite coprime_TIg // (pnat_coprime (pcore_pgroup _ _)) //. apply: sub_in_pnat (pcore_pgroup _ _) => p _ sHp. by apply: contraFN (a2 p) => aMp; rewrite inE /= sHp andbT. have b2: [predI \sigma(M) & \sigma(H)] =i pred0. by move=> p; apply/negP; case/sigmaMHnil => _; rewrite nilMs. rewrite coprime_TIg // (pnat_coprime (pcore_pgroup _ _)) //. apply: sub_in_pnat (pcore_pgroup _ _) => p _ sHp. by apply: contraFN (b2 p) => bMp; rewrite inE /= sHp andbT. case/andP=> sMp sHp; have [S sylS]:= Sylow_exists p M. have [sSM pS _] := and3P sylS. have sylS_G: p.-Sylow(G) S := sigma_Sylow_G maxM sMp sylS. have [g sSHg]: exists g, S \subset H :^ g. have [Sg' sylSg']:= Sylow_exists p H. have [g _ ->] := Sylow_trans (sigma_Sylow_G maxH sHp sylSg') sylS_G. by exists g; rewrite conjSg (pHall_sub sylSg'). have{notjMH} neqHgM: H :^ g != M. by apply: contraNneq notjMH => <-; rewrite orbit_sym mem_orbit ?in_setT. do [split; apply: contra neqHgM] => [|nilMs]. rewrite !inE -(p_rank_Sylow sylS) -rank_pgroup //= => rS_gt3. have uniqS: S \in 'U := rank3_Uniqueness (mFT_pgroup_proper pS) rS_gt3. have defUS: 'M(S) = [set M] := def_uniq_mmax uniqS maxM sSM. by rewrite (eq_uniq_mmax defUS _ sSHg) ?mmaxJ. have nsSM: S <| M. have nsMsM: M`_\sigma <| M by apply: pcore_normal. have{} sylS: p.-Sylow(M`_\sigma) S. apply: pHall_subl (pcore_sub _ _) sylS => //. by rewrite (sub_Hall_pcore (Msigma_Hall maxM)) ?(pi_pgroup pS). by rewrite (nilpotent_Hall_pcore nilMs sylS) gFnormal_trans. have sNS_Hg: 'N(S) \subset H :^ g. rewrite -sub_conjgV -normJ (norm_sigma_Sylow sHp) //. by rewrite (pHall_subl _ (subsetT _)) ?sub_conjgV // pHallJ ?in_setT. have ltHg: H :^ g \proper G by rewrite mmax_proper ?mmaxJ //. rewrite (mmax_max maxM ltHg) // -(mmax_normal maxM nsSM) //. by apply: contraTneq sNS_Hg => ->; rewrite norm1 proper_subn. 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 BGsection9)