proposition: Lemma Ptype_Fcore_kernel_exists : chief_factor M H0 H /\ 'C_H(U) \subset H0.
proof: Proof. pose S := <<class_support 'C_H(U) H>> . suffices [H1 maxH sCH1]: {H1 : {group gT} | maxnormal H1 H M & S \subset H1}. apply/andP; rewrite /H0 /Ptype_Fcore_kernel; case: pickP => // /(_ H1)/idP[]. rewrite /chief_factor maxH Fcore_normal (subset_trans _ sCH1) ?sub_gen //. exact: sub_class_support. apply/maxgroup_exists/andP; split. have snCH: 'C_H(U) <|<| H by rewrite nilpotent_subnormal ?subsetIl. by have [/setIidPl/idPn[] | // ] := subnormalEsupport snCH; rewrite centsC. have [_ {3}<- nHUW1 _] := (sdprodP defHUW1). rewrite norms_gen // mulG_subG class_support_norm norms_class_support //. by rewrite normsI ?norms_cent // join_subG normG. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime binomial ssralg poly finset) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct cyclic commutator center gseries nilpotent) mathcomp(pgroup sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxrepresentation mxabelem vector) odd_order(BGsection1 BGsection3 BGsection7 BGsection15 BGsection16) mathcomp(algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4) odd_order(PFsection5 PFsection6 PFsection8)