proposition: Proposition SCN_Sylow_cent_dprod gT (R G A : {group gT}) p : p.-Sylow(G) R -> A \in 'SCN(R) -> 'O_p^'('C_G(A)) \x A = 'C_G(A).
proof: Proof. move=> sylR scnA; have [[sRG _] [nAR CRA_A]] := (andP sylR, SCN_P scnA). set C := 'C_G(A); have /maxgroupP[/andP[nAG abelA] maxA] := SCN_max scnA. have CiP_eq : C :&: R = A by rewrite -CRA_A setIC setIA (setIidPl sRG). have sylA: p.-Sylow(C) A. rewrite -CiP_eq; apply: (Sylow_setI_normal (subcent_normal _ _)). by apply: pHall_subl sylR; rewrite ?subsetIl // subsetI sRG normal_norm. rewrite dprodEsd; last by rewrite centsC gFsub_trans ?subsetIr. by apply: Burnside_normal_complement; rewrite // subIset ?subsetIr. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype finfun bigop ssralg finset prime binomial) mathcomp(fingroup morphism automorphism perm quotient action gproduct) mathcomp(gfunctor commutator zmodp cyclic center pgroup gseries nilpotent) mathcomp(sylow abelian maximal extremal hall) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(BGsection1 BGsection2)