proposition: Corollary sigma_Hall_tame M H pi x a : M \in 'M -> pi.-Hall(M`_\sigma) H -> x \in H -> x ^ a \in H -> exists2 b, b \in 'N_M(H) & x ^ a = x ^ b.
proof: Proof. move=> maxM hallH Hx Hxa; have [sHMs piH _] := and3P hallH. have SMxM: M \in 'M_\sigma[x] by rewrite inE maxM cycle_subG (subsetP sHMs). have SMxMa: (M :^ a^-1)%G \in 'M_\sigma[x]. by rewrite inE mmaxJ maxM cycle_subG /= MsigmaJ mem_conjgV (subsetP sHMs). have [-> | ntx] := eqVneq x 1; first by exists 1; rewrite ?group1 ?conj1g. have ell1x: \ell_\sigma(x) == 1%N. by apply/ell_sigma1P; split=> //; apply/set0Pn; exists M. have ntH: H :!=: 1 by apply/trivgPn; exists x. have [[transR _ _ _] _] := FT_signalizer_context ell1x. have [c Rc defMc] := atransP2 transR SMxM SMxMa. pose b := c * a; have def_xa: x ^ a = x ^ b. by have [_ cxc] := setIP Rc; rewrite conjgM {3}/conjg -(cent1P cxc) mulKg. have Mb: b \in M. by rewrite -(norm_mmax maxM) inE conjsgM -(congr_group defMc) actKV. have nsMsM: M`_\sigma <| M := pcore_normal _ _; have [sMsM _] := andP nsMsM. have [nsHM | not_nsHM] := boolP (H <| M). by exists b; rewrite // (mmax_normal maxM) ?setIid. have neqMFs: M`_\F != M`_\sigma. apply: contraNneq not_nsHM => /(Fcore_eq_Msigma maxM)nilMs. by rewrite (nilpotent_Hall_pcore nilMs hallH) gFnormal_trans. have [K hallK] := Hall_exists \kappa(M) (mmax_sol maxM). pose q := #|'C_(M`_\sigma)(K)|. have [D hallD] := Hall_exists q^' (solvableS sMsM (mmax_sol maxM)). have [[_ sMFs _ _]] := Fcore_structure maxM; case/(_ K D) => //; rewrite -/q. set Q := 'O_q(M) => _ [_ q_pr piMFq _] [sylQ nilD _] _ _. have sQMs: Q \subset M`_\sigma. by apply: subset_trans sMFs; rewrite -[Q](p_core_Fcore piMFq) pcore_sub. have sylQ_Ms: q.-Hall(M`_\sigma) Q := pHall_subl sQMs sMsM sylQ. have nsQM: Q <| M := pcore_normal q M; have [_ qQ _] := and3P sylQ. have nsQ_Ms: Q <| M`_\sigma := normalS sQMs sMsM nsQM. have defMs: Q ><| D = M`_\sigma := sdprod_normal_p'HallP nsQ_Ms hallD sylQ_Ms. have [_ mulQD nQD tiQD] := sdprodP defMs; rewrite -/Q in mulQD nQD tiQD. have nQH := subset_trans sHMs (normal_norm nsQ_Ms). have nsQHM: Q <*> H <| M. rewrite -(quotientGK nsQM) -quotientYK // cosetpre_normal //= -/Q. suffices ->: H / Q = 'O_pi(M`_\sigma / Q). by rewrite gFnormal_trans ?quotient_normal. apply: nilpotent_Hall_pcore; last exact: quotient_pHall. by rewrite /= -mulQD quotientMidl -(isog_nil (quotient_isog _ _)). have tiQH: Q :&: H = 1. apply: coprime_TIg (p'nat_coprime (pi_pgroup qQ _) piH). apply: contra not_nsHM => pi_q; rewrite (joing_idPr _) // in nsQHM. by rewrite (normal_sub_max_pgroup (Hall_max hallH)) ?(pi_pgroup qQ). have defM: Q * 'N_M(H) = M. have hallH_QH: pi.-Hall(Q <*> H) H. by rewrite (pHall_subl (joing_subr _ _) _ hallH) // join_subG sQMs. have solQH := solvableS (normal_sub nsQHM) (mmax_sol maxM). rewrite -[RHS](Hall_Frattini_arg solQH nsQHM hallH_QH) /= norm_joinEr //. by rewrite -mulgA [H * _]mulSGid // subsetI (subset_trans sHMs sMsM) normG. rewrite -defM in Mb; case/mulsgP: Mb => z n Qz Nn defb; exists n => //. rewrite def_xa defb conjgM [x ^ z](conjg_fixP _) // -in_set1 -set1gE -tiQH. rewrite inE {1}commgEr groupMr // -mem_conjgV groupV /=. rewrite (normsP (normal_norm nsQM)) ?Qz; last first. by rewrite groupV (subsetP sMsM) // (subsetP sHMs). rewrite commgEl groupMl ?groupV //= -(conjsgK n H) mem_conjgV -conjgM -defb. by have [_ nHn] := setIP Nn; rewrite (normP nHn) -def_xa. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq choice div fintype) mathcomp(path bigop finset prime fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor pgroup cyclic commutator) mathcomp(center 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)