proposition: Corollary mFT_rank2_Sylow_cprod : 'r(P) < 3 -> ~~ abelian P -> exists2 S, [/\ ~~ abelian (gval S), logn p #|S| = 3 & exponent S %| p] & exists2 C, cyclic (gval C) & S \* C = P /\ 'Ohm_1(C) = 'Z(S).
proof: Proof. move=> rP not_cPP; have sylP := pHall_subl (normG P) (subsetT 'N(P)) sylP_G. have ntP: P :!=: 1 by apply: contraNneq not_cPP => ->; apply: abelian1. have ltNG: 'N(P) \proper G := mFT_norm_proper ntP (mFT_pgroup_proper pP). have [V hallV] := Hall_exists p^' (mFT_sol ltNG); have [_ p'V _] := and3P hallV. have defNP: P ><| V = 'N(P) := sdprod_normal_p'HallP (normalG P) hallV sylP. have defP: [~: P, V] = P := mFT_Sylow_sdprod_commg defNP. have [_] := rank2_coprime_comm_cprod pP (mFT_odd _) ntP rP defP p'V (mFT_odd _). case=> [/idPn// | [S esS [C [mulSC cycC defC1]]]]. exists S => //; exists C => //; split=> //; rewrite defC1. have sSP: S \subset P by case/cprodP: mulSC => _ /mulG_sub[]. have [[not_cSS dimS _] pS] := (esS, pgroupS sSP pP). by have [||[]] := p3group_extraspecial pS; rewrite ?dimS. 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)