proposition: Theorem Puig_center_normal : 'Z(L) <| G.
proof: Proof. have [sLiST sLTS] := pcore_Sylow_Puig_sub. have sLiLT: 'L_*(T) \subset 'L(T) by apply: Puig_sub_even_odd. have sZY: 'Z(L) \subset Y. rewrite subsetI andbC subIset ?centS ?orbT //=. suffices: 'C_S('L_*(S)) \subset 'L(T). by apply: subset_trans; rewrite setISS ?Puig_sub ?centS ?Puig_sub_even_odd. apply: subset_trans (subset_trans sLiST sLiLT). by apply: sub_cent_Puig_at pS; rewrite double_gt0. have chY: Y \char G by rewrite !gFchar_trans. have nsCY_G: 'C_G(Y) <| G by rewrite char_normal 1?subcent_char ?char_refl. have [C defC sCY_C nsCG] := inv_quotientN nsCY_G (pcore_normal p _). have sLG: L \subset G by rewrite gFsub_trans ?(pHall_sub sylS). have nsL_nCS: L <| 'N_G(C :&: S). have sYLiS: Y \subset 'L_*(S). rewrite abelian_norm_Puig ?double_gt0 ?center_abelian //. apply: normalS (pHall_sub sylS) (char_normal chY). by rewrite subIset // (subset_trans sLTS) ?Puig_sub. have gYL: Y --> L := norm_abgenS sYLiS (Puig_gen _ _). have sLCS: L \subset C :&: S. rewrite subsetI Puig_sub andbT. rewrite -(quotientSGK _ sCY_C) ?(subset_trans sLG) ?normal_norm // -defC. rewrite odd_abelian_gen_stable ?char_normal ?norm_abgen_pgroup //. by rewrite (pgroupS _ pT) ?subIset // Puig_sub. by rewrite (pgroupS _ pS) ?Puig_sub. rewrite -[L](sub_Puig_eq _ sLCS) ?subsetIr // gFnormal_trans ?normalSG //. by rewrite subIset // sSG orbT. have sylCS: p.-Sylow(C) (C :&: S) := Sylow_setI_normal nsCG sylS. have{} defC: 'C_G(Y) * (C :&: S) = C. apply/eqP; rewrite eqEsubset mulG_subG sCY_C subsetIl /=. have nCY_C: C \subset 'N('C_G(Y)). exact: subset_trans (normal_sub nsCG) (normal_norm nsCY_G). rewrite -quotientSK // -defC /= -pseries1. rewrite -(pseries_catr_id [:: p : nat_pred]) (pseries_rcons_id [::]) /=. rewrite pseries1 /= pseries1 defC pcore_sub_Hall // morphim_pHall //. by rewrite subIset ?nCY_C. have defG: 'C_G(Y) * 'N_G(C :&: S) = G. have sCS_N: C :&: S \subset 'N_G(C :&: S). by rewrite subsetI normG subIset // sSG orbT. by rewrite -(mulSGid sCS_N) mulgA defC (Frattini_arg _ sylCS). have nsZ_N: 'Z(L) <| 'N_G(C :&: S) := gFnormal_trans _ nsL_nCS. rewrite /normal subIset ?sLG //= -{1}defG mulG_subG /=. rewrite cents_norm ?normal_norm // centsC. by rewrite (subset_trans sZY) // centsC subsetIr. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div) mathcomp(fintype bigop prime finset ssralg fingroup morphism) mathcomp(automorphism quotient gfunctor commutator zmodp center pgroup) mathcomp(sylow gseries nilpotent abelian maximal) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(BGsection1 BGsection2)