proposition: Proposition p_stable_abelian_constrained : p.-constrained G -> p.-stable G -> p.-abelian_constrained G.
proof: Proof. move=> constrG stabG P A sylP cAA /andP[sAP nAP]. have [sPG pP _] := and3P sylP; have sAG := subset_trans sAP sPG. set K2 := 'O_{p^', p}(G); pose K1 := 'O_p^'(G); pose Q := P :&: K2. have sQG: Q \subset G by rewrite subIset ?sPG. have nK1G: G \subset 'N(K1) by rewrite normal_norm ?pcore_normal. have nsK2G: K2 <| G := pseries_normal _ _; have [sK2G nK2G] := andP nsK2G. have sylQ: p.-Sylow(K2) Q by rewrite /Q setIC (Sylow_setI_normal nsK2G). have defK2: K1 * Q = K2. have sK12: K1 \subset K2 by rewrite /K1 -pseries1 (pseries_sub_catl [::_]). apply/eqP; rewrite eqEsubset mulG_subG /= sK12 subsetIr /=. rewrite -quotientSK ?(subset_trans sK2G) //= quotientIG //= -/K1 -/K2. rewrite subsetI subxx andbT quotient_pseries2. by rewrite pcore_sub_Hall // morphim_pHall // ?(subset_trans sPG). have{cAA} rQAA_1: [~: Q, A, A] = 1. by apply/commG1P; apply: subset_trans cAA; rewrite commg_subr subIset // nAP. have nK2A := subset_trans sAG nK2G. have sAN: A \subset 'N_G(Q) by rewrite subsetI sAG normsI // normsG. have{stabG rQAA_1 defK2 sQG} stabA: A / 'C_G(Q) \subset 'O_p('N_G(Q) / 'C_G(Q)). apply: stabG; rewrite //= /psubgroup -/Q ?sAN ?(pgroupS _ pP) ?subsetIl //. by rewrite defK2 pseries_normal. rewrite -quotient_sub1 //= -/K2 -(setIidPr sAN). have nK2N: 'N_G(Q) \subset 'N(K2) by rewrite subIset ?nK2G. rewrite -[_ / _](morphim_restrm nK2N); set qK2 := restrm _ _. have{constrG} fqKp: 'ker (coset 'C_G(Q)) \subset 'ker qK2. by rewrite ker_restrm !ker_coset subsetI subcent_sub constrG. rewrite -(morphim_factm fqKp (subcent_norm _ _)) -(quotientE A _). apply: subset_trans {stabA}(morphimS _ stabA) _. apply: subset_trans (morphim_pcore _ _ _) _. rewrite morphim_factm morphim_restrm setIid -quotientE. rewrite /= -quotientMidl /= -/K2 (Frattini_arg _ sylQ) ?pseries_normal //. by rewrite -quotient_pseries //= (pseries_rcons_id [::_]) trivg_quotient. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div fintype) mathcomp(bigop prime binomial finset fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor commutator) mathcomp(ssralg finalg zmodp cyclic center pgroup finmodule gseries) mathcomp(nilpotent sylow abelian maximal hall extremal) mathcomp(matrix mxalgebra mxrepresentation mxabelem)