proposition: Lemma Ptype_Fcore_extensions_normal : [/\ H0C <| M, HC <| M, H0U' <| M & H0C' <| M].
proof: Proof. have [nsHUM sW1M /mulG_sub[sHUM _] nHUW1 tiHUW1] := sdprod_context defM. have [nsHHU sUHU /mulG_sub[sHHU _] nHU tiHU] := sdprod_context defHU. have [sHM sUM] := (subset_trans sHHU sHUM, subset_trans sUHU sHUM). have sCM: C \subset M := subset_trans sCU sUM. have sH0C_M: H0C \subset M by rewrite /normal join_subG (subset_trans sH0H). have [nH0C nH0_H0C] := (subset_trans sCM nH0M, subset_trans sH0C_M nH0M). have nsH0C: H0C <| M. rewrite /normal sH0C_M -{1}defM sdprodEY //= -defHU sdprodEY //= -joingA. rewrite join_subG andbC normsY ?(normal_norm nsCUW1) //=; last first. by rewrite (subset_trans _ nH0M) // join_subG sUM. rewrite -quotientYK // -{1}(quotientGK nsH0H) morphpre_norms //= [C]unlock. by rewrite cents_norm // centsC -quotient_astabQ quotientS ?subsetIr. split=> //; first by rewrite /= -{1}(joing_idPl sH0H) -joingA normalY ?gFnormal. rewrite normalY // /normal gFsub_trans //=. rewrite -defM sdprodEY //= -defHU sdprodEY //=. by rewrite !join_subG gFnorm cents_norm ?gFnorm_trans // centsC. suffices ->: H0C' :=: H0 <*> H0C^`(1) by rewrite normalY ?gFnormal_trans. by rewrite /= -!quotientYK ?gFsub_trans ?quotient_der ?subsetIl //= cosetpreK. 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)