proposition: Corollary narrow_centP : reflect (exists S, [/\ gval S \subset R, #|S| = p & 'r_p('C_R(S)) <= 2]) (p.-narrow R).
proof: Proof. rewrite /narrow rR; apply: (iffP (set0Pn _)) => [[E maxEp2E]|[S [sSR oS rCRS]]]. have [Ep2E maxE] := setIP maxEp2E. have{maxEp2E} [_ [oZ _] _] := Ohm1_ucn_p2maxElem maxEp2E. have [sER abelE dimE] := pnElemP Ep2E; have oE := card_pnElem Ep2E. have sZE: Z \subset E by rewrite -(Ohm1_cent_max maxE pR) OhmS ?setIS ?centS. have [S defE] := abelem_split_dprod abelE sZE; exists S. have{defE} [[_ defZS _ _] oZS] := (dprodP defE, dprod_card defE). split; first by rewrite (subset_trans _ sER) // -defZS mulG_subr. by apply/eqP; rewrite -(eqn_pmul2l (ltnW p_gt1)) -{1}oZ oZS oE. rewrite -dimE -p_rank_abelem // -(Ohm1_cent_max maxE pR) p_rank_Ohm1. by rewrite -defZS /= centM setIA defCRZ. have abelS := prime_abelem p_pr oS. have cSZ: Z \subset 'C(S) by rewrite (centsS sSR) // centsC -defCRZ subsetIr. have sSZR: S <*> Z \subset R by rewrite join_subG sSR. have defSZ: S \x Z = S <*> Z. rewrite dprodEY ?prime_TIg ?oS //= -/Z; apply: contraL rR => sSZ. by rewrite -leqNgt (leq_trans _ rCRS) ?p_rankS // -{1}defCRZ setIS ?centS. have abelSZ: p.-abelem (S <*> Z) by rewrite (dprod_abelem p defSZ) abelS. have [pSZ cSZSZ _] := and3P abelSZ. have dimSZ: logn p #|S <*> Z| = 2. apply/eqP; rewrite -p_rank_abelem // eqn_leq (leq_trans (p_rankS _ _) rCRS). rewrite -(p_rank_dprod p defSZ) p_rank_abelem // oS (pfactorK 1) // ltnS. by rewrite -rank_pgroup // rank_gt0. by rewrite subsetI sSZR sub_abelian_cent ?joing_subl. exists [group of S <*> Z]; rewrite 3!inE sSZR abelSZ dimSZ /=. apply/pmaxElemP; rewrite inE sSZR; split=> // E; case/pElemP=> sER abelE sSZE. apply: contraTeq rCRS; rewrite eq_sym -ltnNge -dimSZ => neqSZE. have [[pE cEE _] sSE] := (and3P abelE, subset_trans (joing_subl S Z) sSZE). rewrite (leq_trans (properG_ltn_log pE _)) ?properEneq ?neqSZE //. by rewrite -p_rank_abelem ?p_rankS // subsetI sER sub_abelian_cent. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype finset prime fingroup morphism perm automorphism action) mathcomp(quotient cyclic gfunctor pgroup gproduct center commutator) mathcomp(gseries nilpotent sylow abelian maximal hall) odd_order(BGsection1 BGsection4)