proposition: Corollary tau1_act_tau2 M E p A q Q (Ms := M`_\sigma) : M \in 'M -> \sigma(M)^'.-Hall(M) E -> p \in \tau2(M) -> A \in 'E_p^2(E) -> q \in \tau1(M) -> Q \in 'E_q^1(E) -> 'C_Ms(Q) = 1 -> [~: A, Q] != 1 -> let A0 := [~: A, Q]%G in let A1 := ('C_A(Q))%G in [/\ [/\ A0 \in 'E_p^1(A), 'C_A(Ms) = A0 & A0 <| M], gval A0 \notin A1 :^: G & A1 \in 'E_p^1(A) /\ ~~ ('C(A1) \subset M)].
proof: Proof. move=> maxM hallE t2Mp Ep2A t1Mq EqQ regQ ntA0 A0 A1. have [sEM sM'E _] := and3P hallE. have [sAE abelA dimA] := pnElemP Ep2A; have [pA cAA _] := and3P abelA. have [sQE abelQ dimQ] := pnElemP EqQ; have [qQ _ _] := and3P abelQ. have [p_pr q_pr] := (pnElem_prime Ep2A, pnElem_prime EqQ). have p_gt1 := prime_gt1 p_pr. have Ep2A_M := subsetP (pnElemS p 2 sEM) A Ep2A. have [_ _ regA _ _] := tau2_context maxM t2Mp Ep2A_M. have [[nsAE _] _ _ _] := tau2_compl_context maxM hallE t2Mp Ep2A. have [_ nAE] := andP nsAE; have nAQ := subset_trans sQE nAE. have coAQ: coprime #|A| #|Q|. exact: sub_pnat_coprime tau2'1 (pi_pnat pA t2Mp) (pi_pnat qQ t1Mq). have defA: A0 \x A1 = A := coprime_abelian_cent_dprod nAQ coAQ cAA. have [_ _ _ tiA01] := dprodP defA. have [sAM sM'A] := (subset_trans sAE sEM, pgroupS sAE sM'E). have sM'q: q \in \sigma(M)^' by case/andP: t1Mq. have EqQ_NA: Q \in 'E_q^1('N_M(A)). by apply: subsetP EqQ; rewrite pnElemS // subsetI sEM. have q'A: q^'.-group A. rewrite p'groupEpi ?coprime_pi' // in coAQ *. by apply: (pnatPpi coAQ); rewrite -p_rank_gt0 (p_rank_abelem abelQ) dimQ. have [] := commG_sigma'_1Elem_cyclic maxM sAM sM'A sM'q EqQ_NA regQ q'A cAA. rewrite -[[~: A, Q]]/(gval A0) -/Ms => cMsA0 cycA0 nsA0M. have sA0A: A0 \subset A by rewrite commg_subl. have EpA0: A0 \in 'E_p^1(A). have abelA0 := abelemS sA0A abelA; have [pA0 _] := andP abelA0. rewrite p1ElemE // !inE sA0A -(Ohm1_id abelA0) /=. by rewrite (Ohm1_cyclic_pgroup_prime cycA0 pA0). have defA0: 'C_A(Ms) = A0. apply/eqP; rewrite eq_sym eqEcard subsetI sA0A cMsA0 (card_pnElem EpA0). have pCAMs: p.-group 'C_A(Ms) := pgroupS (subsetIl A _) pA. rewrite (card_pgroup pCAMs) leq_exp2l //= leqNgt. apply: contra (Msigma_neq1 maxM) => dimCAMs. rewrite eq_sym -regA (sameP eqP setIidPl) centsC (sameP setIidPl eqP). by rewrite eqEcard subsetIl (card_pnElem Ep2A) (card_pgroup pCAMs) leq_exp2l. have EpA1: A1 \in 'E_p^1(A). rewrite p1ElemE // !inE subsetIl -(eqn_pmul2l (ltnW p_gt1)). by rewrite -{1}[p](card_pnElem EpA0) (dprod_card defA) (card_pnElem Ep2A) /=. have defNA0: 'N(A0) = M by apply: mmax_normal. have not_cA0Q: ~~ (Q \subset 'C(A0)). apply: contra ntA0 => cA0Q. by rewrite -subG1 -tiA01 !subsetI subxx sA0A centsC cA0Q. have rqM: 'r_q(M) = 1%N by apply/eqP; case/and3P: t1Mq. have q'CA0: q^'.-group 'C(A0). have [S sylS sQS] := Sylow_superset (subset_trans sQE sEM) qQ. have qS := pHall_pgroup sylS; rewrite -(p_rank_Sylow sylS) in rqM. have cycS: cyclic S by rewrite (odd_pgroup_rank1_cyclic qS) ?mFT_odd ?rqM. have ntS: S :!=: 1 by rewrite -rank_gt0 (rank_pgroup qS) rqM. have defS1: 'Ohm_1(S) = Q. apply/eqP; rewrite eq_sym eqEcard -{1}(Ohm1_id abelQ) OhmS //=. by rewrite (card_pnElem EqQ) (Ohm1_cyclic_pgroup_prime cycS qS). have sylSC: q.-Sylow('C(A0)) 'C_S(A0). by rewrite (Hall_setI_normal _ sylS) // -defNA0 cent_normal. rewrite -partG_eq1 ?cardG_gt0 // -(card_Hall sylSC) -trivg_card1 /=. by rewrite setIC TI_Ohm1 // defS1 setIC prime_TIg ?(card_pnElem EqQ). do 2?split=> //. have: ~~ q^'.-group Q by rewrite /pgroup (card_pnElem EqQ) pnatE ?inE ?negbK. apply: contra; case/imsetP=> x _ defA01. rewrite defA01 centJ pgroupJ in q'CA0. by apply: pgroupS q'CA0; rewrite centsC subsetIr. have [S sylS sAS] := Sylow_superset (subsetT A) pA. have [cSS | not_cSS] := boolP (abelian S). have solE := sigma_compl_sol hallE. have [E1 hallE1 sQE1] := Hall_superset solE sQE (pi_pnat qQ t1Mq). have [E3 hallE3] := Hall_exists \tau3(M) solE. have [E2 _ complEi] := ex_tau2_compl hallE hallE1 hallE3. have [_ _ _ reg1Z] := abelian_tau2 maxM complEi t2Mp Ep2A sylS sAS cSS. have E1Q: Q \in 'E^1(E1). by apply/nElemP; exists q; rewrite // !inE sQE1 abelQ dimQ. rewrite (subset_trans (reg1Z Q E1Q regQ)) ?subIset // in not_cA0Q. by rewrite centS ?orbT // (subset_trans sA0A). have pS := pHall_pgroup sylS. have [_ _ not_cent_reg _] := nonabelian_tau2 maxM hallE t2Mp Ep2A pS not_cSS. case: (not_cent_reg A1); rewrite // 2!inE (subsetP (pnElemS p 1 sAE)) // andbT. by rewrite -val_eqE /= defA0 eq_sym; apply/(TIp1ElemP EpA0 EpA1). 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 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9 BGsection10 BGsection11)