proposition: Corollary tau1_cent_tau2Elem_factor M E p A : M \in 'M -> \sigma(M)^'.-Hall(M) E -> p \in \tau2(M) -> A \in 'E_p^2(E) -> [/\ forall E1 E2 E3, sigma_complement M E E1 E2 E3 -> E3 * E2 \subset 'C_E(A), 'C_E(A) <| E & \tau1(M).-group (E / 'C_E(A))].
proof: Proof. move=> maxM hallE t2p Ep2A; have sEM: E \subset M := pHall_sub hallE. have nsAE: A <| E by case/(tau2_compl_context maxM): Ep2A => //; case. have [sAE nAE]: A \subset E /\ E \subset 'N(A) := andP nsAE. have nsCAE: 'C_E(A) <| E by rewrite norm_normalI ?norms_cent. have [[E1 hallE1] [E3 hallE3]] := ex_tau13_compl hallE. have [E2 hallE2 complEi] := ex_tau2_compl hallE hallE1 hallE3. have{hallE1} [t1E1 sE3E] := (pHall_pgroup hallE1, pHall_sub hallE3). have{nsAE} sAE2: A \subset E2. apply: subset_trans (pcore_max _ nsAE) (pcore_sub_Hall hallE2). by apply: pi_pnat t2p; case/pnElemP: Ep2A => _; case/andP. have{complEi} defE: (E3 ><| E2) ><| E1 = E. by case/sigma_compl_context: complEi => // _ _ _ [_ ->]. have [[K _ defK _] _ _ _] := sdprodP defE; rewrite defK in defE. have nsKE: K <| E by case/sdprod_context: defE. have [[sKE nKE] [_ mulE32 nE32 tiE32]] := (andP nsKE, sdprodP defK). have{sE3E} sK_CEA: K \subset 'C_E(A). have cE2E2: abelian E2 := tau2_compl_abelian maxM hallE hallE2. rewrite subsetI sKE -mulE32 mulG_subG (centsS sAE2 cE2E2) (sameP commG1P eqP). rewrite -subG1 -tiE32 subsetI commg_subl (subset_trans sAE2) //=. by rewrite (subset_trans _ sAE2) // commg_subr (subset_trans sE3E). split=> // [_ F2 F3 [_ _ hallF2 hallF3 _] | ]. have solE: solvable E := solvableS sEM (mmax_sol maxM). have [x2 Ex2 ->] := Hall_trans solE hallF2 hallE2. have [x3 Ex3 ->] := Hall_trans solE hallF3 hallE3. rewrite mulG_subG !sub_conjg !(normsP (normal_norm nsCAE)) ?groupV //. by rewrite -mulG_subG mulE32. have [f <-] := homgP (homg_quotientS nKE (normal_norm nsCAE) sK_CEA). by rewrite morphim_pgroup // /pgroup -divg_normal // -(sdprod_card defE) mulKn. 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)