proposition: Lemma sigma'1Elem_sub_p2Elem X : X \in 'E_p^1(G) -> 'N(X) \subset M -> exists2 A, A \in 'E_p^2(G) & X \subset A.
proof: Proof. move=> EpX sNXM; have sXM := subset_trans (normG X) sNXM. have [[_ abelX dimX] p_pr] := (pnElemP EpX, pnElem_prime EpX). have pX := abelem_pgroup abelX; have rpM2 := sigma'_norm_mmax_rank2 pX sNXM. have [P sylP sXP] := Sylow_superset sXM pX; have [sPM pP _] := and3P sylP. pose T := 'Ohm_1('Z(P)); pose A := X <*> T; have nilP := pgroup_nil pP. have charT: T \char P by apply/gFchar_trans/gFchar. have neqTX: T != X. apply: contraNneq s'p => defX; apply/exists_inP; exists P => //. by rewrite (subset_trans _ sNXM) // -defX char_norms. have rP: 'r(P) = 2 by rewrite (rank_Sylow sylP) rpM2. have ntT: T != 1 by rewrite Ohm1_eq1 center_nil_eq1 // -rank_gt0 rP. have sAP: A \subset P by rewrite join_subG sXP char_sub. have cTX: T \subset 'C(X) := centSS (Ohm_sub 1 _) sXP (subsetIr P _). have{cTX} defA: X \* T = A by rewrite cprodEY. have{defA} abelA : p.-abelem A. have pZ: p.-group 'Z(P) := pgroupS (center_sub P) pP. by rewrite (cprod_abelem _ defA) abelX Ohm1_abelem ?center_abelian. exists [group of A]; last exact: joing_subl. rewrite !inE subsetT abelA eqn_leq -{1}rP -{1}(rank_abelem abelA) rankS //=. rewrite -dimX (properG_ltn_log (pgroupS sAP pP)) // /proper join_subG subxx. rewrite joing_subl /=; apply: contra ntT => sTX; rewrite eqEsubset sTX in neqTX. by rewrite -(setIidPr sTX) prime_TIg ?(card_pnElem EpX). 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)