proposition: Lemma injm_pmaxElem p (E : {group aT}) : E \subset D -> ((f @* E)%G \in 'E*_p(f @* G)) = (E \in 'E*_p(G)).
proof: Proof. move=> sED; have defE := morphim_invm injf sED. apply/pmaxElemP/pmaxElemP=> [] [EpE maxE]. split=> [|H EpH sEH]; first by rewrite injm_pElem in EpE. have sHD: H \subset D by apply: subset_trans (sGD); case/pElemP: EpH. by rewrite -(morphim_invm injf sHD) [f @* H]maxE ?morphimS ?injm_pElem. rewrite injm_pElem //; split=> // fH Ep_fH sfEH; have [sfHG _] := pElemP Ep_fH. have sfHD : fH \subset f @* D by rewrite (subset_trans sfHG) ?morphimS. rewrite -(morphpreK sfHD); congr (f @* _). rewrite [_ @*^-1 fH]maxE -?sub_morphim_pre //. by rewrite -injm_pElem ?subsetIl // (group_inj (morphpreK sfHD)). Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism action) mathcomp(quotient gfunctor gproduct ssralg countalg finalg zmodp) mathcomp(cyclic pgroup gseries nilpotent sylow)