proposition: Remark of_typeP_conj (Ux W1x W2x Wx : {group gT}) (defWx : W1x \x W2x = Wx) : of_typeP M Ux defWx -> exists x, [/\ x \in M, U :^ x = Ux, W1 :^ x = W1x, W2 :^ x = W2x & W :^ x = Wx].
proof: Proof. move=> MtypePx; have [[_ _ _ defMx] [_ _ nUW1x defM'x] _ _ _] := MtypePx. have [[_ hallW1 _ defM] [_ _ nUW1 defM'] _ _ _] := MtypeP. have [/mulG_sub[/= sHM' sUM'] [_ _ nM'W1 _]] := (sdprodW defM', sdprodP defM). rewrite -/M' -/H in defMx defM'x defM defM' sHM' sUM' nM'W1. have /imsetP[x2 Mx2 defW1x2] := of_typeP_compl_conj MtypeP defMx. have /andP[sM'M nM'M]: M' <| M by apply: der_normal. have solM': solvable M' := solvableS sM'M (of_typeP_sol MtypeP). have [hallU hallUx]: \pi(H)^'.-Hall(M') U /\ \pi(H)^'.-Hall(M') (Ux :^ x2^-1). have hallH: \pi(H).-Hall(M') H by apply: pHall_subl (Fcore_Hall M). rewrite pHallJnorm ?(subsetP nM'M) ?groupV // -!(compl_pHall _ hallH). by rewrite (sdprod_compl defM') (sdprod_compl defM'x). have coM'W1: coprime #|M'| #|W1| by rewrite (coprime_sdprod_Hall_r defM). have nUxW1: W1 \subset 'N(Ux :^ x2^-1) by rewrite normJ -sub_conjg -defW1x2. have [x1] := coprime_Hall_trans nM'W1 coM'W1 solM' hallUx nUxW1 hallU nUW1. case/setIP=> /(subsetP sM'M) My /(normsP (cent_sub _)) nW1x1 defUx1. pose x := (x1 * x2)%g; have Mx: x \in M by rewrite groupM. have defW1x: W1 :^ x = W1x by rewrite conjsgM nW1x1. have defW2x: W2 :^ x = W2x. rewrite -(typeP_cent_compl MtypeP) -(typeP_cent_compl MtypePx). by rewrite conjIg -centJ defW1x (normsP nM'M). by exists x; rewrite -defW dprodJ defW1x defW2x conjsgM -defUx1 conjsgKV. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice) mathcomp(fintype tuple finfun bigop prime ssralg poly finset center) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct cyclic commutator nilpotent pgroup) mathcomp(sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxrepresentation vector) odd_order(BGsection1 BGsection3 BGsection7 BGsection10) odd_order(BGsection14 BGsection15 BGsection16) mathcomp(algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4 PFsection5)