proposition: Theorem exceptional_mul_sigma_normal : M`_\sigma <*> A <| M.
proof: Proof. set Ms := M`_\sigma; have pP := pHall_pgroup sylP; have solM := mmax_sol maxM. have [E hallE sPE] := Hall_superset solM sPM (pi_pnat pP sM'p). have sAE := subset_trans sAP sPE; have [sEM s'E _] := and3P hallE. have [_ _ dimA] := pnElemP Ep2A. have rE: 'r(E) = 2. apply/eqP; rewrite eqn_leq -{2}dimA -rank_abelem ?rankS // andbT leqNgt. have [q q_pr ->]:= rank_witness E; apply/negP=> rqEgt2. have piEq: q \in \pi(E) by rewrite -p_rank_gt0 -(subnKC rqEgt2). case/negP: (pnatPpi s'E piEq); rewrite /= alpha_sub_sigma // !inE. by rewrite (leq_trans rqEgt2) ?p_rankS. have rFEle2: 'r('F(E)) <= 2 by rewrite -rE rankS ?Fitting_sub. have solE := solvableS sEM solM; have oddE := mFT_odd E. pose tau : nat_pred := [pred q | q > p]; pose K := 'O_tau(E). have hallK: tau.-Hall(E) K by rewrite rank2_ge_pcore_Hall. pose ptau : nat_pred := [pred q | q >= p]; pose KP := K <*> P. have nKP: P \subset 'N(K) by rewrite (subset_trans sPE) ?gFnorm. have coKP: coprime #|K| #|P|. by rewrite (pnat_coprime (pcore_pgroup _ _)) ?(pi_pnat pP) //= !inE ltnn. have hallKP: ptau.-Hall(E) KP. rewrite pHallE join_subG pcore_sub sPE /= norm_joinEr ?coprime_cardMg //. apply/eqP; rewrite -(partnC tau (part_gt0 _ _)) (card_Hall sylP). rewrite (card_Hall hallK) partn_part => [|q]; last exact: leqW. rewrite (card_Hall hallE) -!partnI; congr (_ * _)%N; apply: eq_partn => q. rewrite [\sigma(M)^']lock !inE -lock -leqNgt -eqn_leq eq_sym andb_idl //. by move/eqP <-. have nsKP_E: KP <| E. by rewrite [KP](eq_Hall_pcore _ hallKP) ?pcore_normal ?rank2_ge_pcore_Hall. have [cKA | not_cKA]:= boolP (A \subset 'C(K)). pose KA := K <*> A; have defKA: K \x A = KA. by rewrite dprodEY // coprime_TIg // (coprimegS sAP). have defA: 'Ohm_1(P) = A by case exceptional_structure. have{} defA: 'Ohm_1('O_p(KP)) = A. apply/eqP; rewrite -defA eqEsubset OhmS /=; last first. rewrite pcore_sub_Hall ?(pHall_subl _ _ sylP) ?joing_subr //. exact: subset_trans (pHall_sub hallKP) sEM. rewrite -Ohm_id defA OhmS // pcore_max // /normal join_subG. rewrite (subset_trans sAP) ?joing_subr // cents_norm 1?centsC //=. by rewrite -defA gFnorm. have nMsE: E \subset 'N(Ms) by rewrite (subset_trans sEM) ?gFnorm. have tiMsE: Ms :&: E = 1. by rewrite coprime_TIg ?(pnat_coprime (pcore_pgroup _ _)). have <-: Ms * E = M. apply/eqP; rewrite eqEcard mulG_subG pcore_sub sEM /= TI_cardMg //. by rewrite (card_Hall hallE) (card_Hall (Msigma_Hall maxM)) ?partnC. rewrite norm_joinEr -?quotientK ?(subset_trans sAE) //= cosetpre_normal. by rewrite quotient_normal // -defA !gFnormal_trans. pose q := pdiv #|K : 'C_K(A)|. have q_pr: prime q by rewrite pdiv_prime // indexg_gt1 subsetI subxx centsC. have [nKA coKA] := (subset_trans sAP nKP, coprimegS sAP coKP). have [Q sylQ nQA]: exists2 Q : {group gT}, q.-Sylow(K) Q & A \subset 'N(Q). by apply: sol_coprime_Sylow_exists => //; apply: (pgroup_sol pA). have [sQK qQ q'iQK] := and3P sylQ; have [sKE tauK _]:= and3P hallK. have{q'iQK} not_cQA: ~~ (A \subset 'C(Q)). apply: contraL q'iQK => cQA; rewrite p'natE // negbK. rewrite -(Lagrange_index (subsetIl K 'C(A))) ?dvdn_mulr ?pdiv_dvd //. by rewrite subsetI sQK centsC. have ntQ: Q :!=: 1 by apply: contraNneq not_cQA => ->; apply: cents1. have q_dv_K: q %| #|K| := dvdn_trans (pdiv_dvd _) (dvdn_indexg _ _). have sM'q: q \in (\sigma(M))^' := pgroupP (pgroupS sKE s'E) q q_pr q_dv_K. have{q_dv_K} tau_q: q \in tau := pgroupP tauK q q_pr q_dv_K. have sylQ_E: q.-Sylow(E) Q := subHall_Sylow hallK tau_q sylQ. have sylQ_M: q.-Sylow(M) Q := subHall_Sylow hallE sM'q sylQ_E. have q'p: p != q by rewrite neq_ltn [p < q]tau_q. suffices nregQ: 'C_Q(A) != 1. have ncycQ: ~~ cyclic Q. apply: contra not_cQA => cycQ. rewrite (coprime_odd_faithful_Ohm1 qQ) ?mFT_odd ?(coprimeSg sQK) //. rewrite centsC; apply: contraR nregQ => not_sQ1_CA. rewrite setIC TI_Ohm1 // setIC prime_TIg //. by rewrite (Ohm1_cyclic_pgroup_prime cycQ qQ ntQ). have {ncycQ} rQ: 'r_q(Q) = 2. apply/eqP; rewrite eqn_leq ltnNge -odd_pgroup_rank1_cyclic ?mFT_odd //. by rewrite -rE -rank_pgroup ?rankS // (pHall_sub sylQ_E). have [B Eq2B]: exists B, B \in 'E_q^2(Q) by apply/p_rank_geP; rewrite rQ. have maxB: B \in 'E*_q(G). apply: subsetP (subsetP (pnElemS q 2 (pHall_sub sylQ_M)) B Eq2B). by rewrite sigma'_rank2_max // -(p_rank_Sylow sylQ_M). have CAq: q %| #|'C(A)|. apply: dvdn_trans (cardSg (subsetIr Q _)). by have [_ ? _] := pgroup_pdiv (pgroupS (subsetIl Q _) qQ) nregQ. have [Qstar maxQstar sQ_Qstar] := max_normed_exists qQ nQA. have [|Qm] := max_normed_2Elem_signaliser q'p _ maxQstar CAq. by rewrite inE (subsetP (pnElemS p 2 (subsetT M))). case=> _ sAQm [_ _ cQstarQm]; rewrite (centSS sAQm sQ_Qstar) // in not_cQA. apply: cQstarQm; apply/implyP=> _; apply/set0Pn; exists B. have{} Eq2B := subsetP (pnElemS q 2 sQ_Qstar) B Eq2B. rewrite inE Eq2B (subsetP (pmaxElemS q (subsetT _))) // inE maxB inE. by have [? _ _] := pnElemP Eq2B. pose Q0 := 'Z(Q); have sQ0Q: Q0 \subset Q by apply: gFsub. have nQ0A: A \subset 'N(Q0) by apply: gFnorm_trans. have ntQ0: Q0 != 1 by apply: contraNneq ntQ => /(trivg_center_pgroup qQ)->. apply: contraNneq (sM'q) => regQ; apply/exists_inP; exists Q => //. suffices nsQ0M: Q0 <| M by rewrite -(mmax_normal _ nsQ0M) ?gFnorms. have sQ0M: Q0 \subset M := subset_trans sQ0Q (pHall_sub sylQ_M). have qQ0: q.-group Q0 := pgroupS sQ0Q qQ. have p'Q0: p^'.-group Q0 by apply: (pi_pnat qQ0); rewrite eq_sym in q'p. have sM'Q0: \sigma(M)^'.-group Q0 := pi_pnat qQ0 sM'q. have cQ0Q0: abelian Q0 := center_abelian Q. have defQ0: [~: A, Q0] = Q0. rewrite -{2}[Q0](coprime_abelian_cent_dprod nQ0A) //. by rewrite setIAC regQ setI1g dprodg1 commGC. by rewrite (coprimeSg (subset_trans sQ0Q sQK)). have [_ _ [A1 EpA1 [A2 EpA2 [neqA12 regA1 regA2]]]] := exceptional_structure. have defA: A1 \x A2 = A by apply/(p2Elem_dprodP Ep2A EpA1 EpA2). have{} defQ0: [~: A1, Q0] * [~: A2, Q0] = Q0. have{defA} [[_ defA cA12 _] [sA2A _ _]] := (dprodP defA, pnElemP EpA2). by rewrite -commMG ?defA // normsR ?(cents_norm cA12) // (subset_trans sA2A). have sA_NQ0: A \subset 'N_M(Q0) by rewrite subsetI sAM. have sEpA_EpN := subsetP (pnElemS p 1 sA_NQ0). have nsRQ0 := commG_sigma'_1Elem_cyclic maxM sQ0M sM'Q0 sM'p (sEpA_EpN _ _). rewrite -defQ0 -!(commGC Q0). by apply: normalM; [case/nsRQ0: EpA1 | case/nsRQ0: EpA2]. 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)