proposition: Theorem narrow_cent_dprod S : p.-narrow R -> #|S| = p -> S \subset R -> 'r_p('C_R(S)) <= 2 -> [/\ cyclic 'C_T(S), S :&: R^`(1) = 1, S :&: T = 1 & S \x 'C_T(S) = 'C_R(S)].
proof: Proof. move=> nnR oS sSR rS; have pS : p.-group S := pgroupS sSR pR. have [E maxEp2E] := narrow_pmaxElem nnR; have [Ep2E maxE] := setIP maxEp2E. have [not_sET [oZ Ep2W] [charT maxT]] := Ohm1_ucn_p2maxElem maxEp2E. have cZS : S \subset 'C(Z) by rewrite (subset_trans sSR) // -defCRZ subsetIr. have nZS : S \subset 'N(Z) by rewrite cents_norm. have cSS : abelian S by rewrite cyclic_abelian ?prime_cyclic // oS. pose SZ := (S <*> [group of Z])%G; have sSSZ: S \subset SZ := joing_subl _ _. have sSZ_R: SZ \subset R by rewrite join_subG sSR sZR. have abelSZ : p.-abelem SZ. by rewrite /= joingC (cprod_abelem p (cprodEY cZS)) abelZ prime_abelem. have tiSZ: S :&: Z = 1. rewrite prime_TIg ?oS //= -/Z; apply: contraL rR => sZS. by rewrite -leqNgt (leq_trans _ rS) ?p_rankS // -{1}defCRZ setIS ?centS. have{tiSZ} oSZ: #|SZ| = (p ^ 2)%N by rewrite /= norm_joinEl ?TI_cardMg ?oS ?oZ. have Ep2SZ: SZ \in 'E_p^2(R) by rewrite pnElemE // !inE sSZ_R abelSZ oSZ eqxx. have{oSZ Ep2SZ abelSZ sSZ_R} maxSZ: SZ \in 'E_p^2(R) :&: 'E*_p(R). rewrite inE Ep2SZ; apply/pmaxElemP; rewrite inE sSZ_R abelSZ. split=> // H /setIdP[sHR abelH] sSZH. have [[_ _ dimSZ] [cHH pH _]] := (pnElemP Ep2SZ, and3P abelH). have sSH: S \subset H := subset_trans sSSZ sSZH. have{sSH} sH_CRS: H \subset 'C_R(S) by rewrite subsetI sHR (centsS sSH). have{sH_CRS}: 'r_p(H) <= 2 by rewrite (leq_trans _ rS) ?p_rankS. apply: contraTeq; rewrite eq_sym eqEproper sSZH negbK => lSZH. by rewrite -ltnNge p_rank_abelem // -dimSZ properG_ltn_log. have sZT: Z \subset T. by rewrite subsetI sZR (centsS sWR) // centsC -defCRZ subsetIr. have{SZ sSSZ maxSZ} not_sST: ~~ (S \subset T). have: ~~ (SZ \subset T) by case/Ohm1_ucn_p2maxElem: maxSZ. by rewrite join_subG sZT andbT. have tiST: S :&: T :=: 1 by rewrite prime_TIg ?oS. have defST: S * T = R. apply/eqP; rewrite eqEcard TI_cardMg ?mul_subG ?subsetIl //=. by rewrite mulnC oS -maxT Lagrange ?subsetIl. have cRRb: abelian (R / T) by rewrite -defST quotientMidr quotient_abelian. have sR'T: R^`(1) \subset T by rewrite der1_min ?char_norm. have TI_SR': S :&: R^`(1) :=: 1. by rewrite prime_TIg ?oS // (contra _ not_sST) // => /subset_trans->. have defCRS : S \x 'C_T(S) = 'C_R(S). rewrite (dprodE _ _) ?subsetIr //= -/T; last by rewrite setIA tiST setI1g. rewrite -{1}(center_idP cSS) subcent_TImulg ?defST //. by rewrite subsetI normG (subset_trans sSR) ?char_norm. have sCTSR: 'C_T(S) \subset R by rewrite subIset ?subsetIl. split; rewrite ?(odd_pgroup_rank1_cyclic (pgroupS _ pR) (oddSg _ oddR)) //= -/T. rewrite -ltnS (leq_trans _ rS) //= -(p_rank_dprod p defCRS) -add1n leq_add2r. by rewrite -rank_pgroup // rank_gt0 -cardG_gt1 oS. 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)