proposition: Theorem normed_trans_superset P : A <|<| P -> pi.-group P -> [transitive K, on |/|*(A; q) | 'JG] -> [/\ 'C_K(P) = 'O_pi^'('C(P)), [transitive 'O_pi^'('C(P)), on |/|*(P; q) | 'JG], |/|*(P; q) \subset |/|*(A; q) & {in |/|*(P; q), forall Q, P :&: 'N(P)^`(1) \subset 'N(Q)^`(1) /\ 'N(P) = 'C_K(P) * 'N_('N(P))(Q)}].
proof: Proof. move=> snAP piP trnK; set KP := 'O_pi^'('C(P)). have defK B: A \subset B -> 'C_K(B) = 'O_pi^'('C(B)). move=> sAB; apply/eqP; rewrite eqEsubset {1}setIC pcoreS ?centS // subsetI. by rewrite gFsub (sub_Hall_pcore hallK) ?pcore_pgroup // gFsub_trans ?centS. suffices: [transitive KP, on |/|*(P; q) | 'JG] /\ |/|*(P; q) \subset |/|*(A; q). have nsKPN: KP <| 'N(P) := gFnormal_trans _ (cent_normal _). case=> trKP smnPA; rewrite (defK _ (subnormal_sub snAP)); split=> // Q maxQ. have defNP: KP * 'N_('N(P))(Q) = 'N(P). rewrite -(astab1JG Q) -normC; last by rewrite subIset 1?normal_norm. apply/(subgroup_transitiveP maxQ); rewrite ?normal_sub //=. by rewrite (atrans_supgroup _ trKP) ?norm_acts_max_norm ?normal_sub. split=> //; move/pprod_focal_coprime: defNP => -> //. - by rewrite subIset // orbC commgSS ?subsetIr. - by rewrite subsetI normG; case/mem_max_normed: maxQ. by rewrite (p'nat_coprime (pcore_pgroup _ _)). elim: {P}_.+1 {-2}P (ltnSn #|P|) => // m IHm P lePm in KP piP snAP *. wlog{snAP} [B maxnB snAB]: / {B : grT | maxnormal B P P & A <|<| B}. case/subnormalEr: snAP => [|[D [snAD nDP prDP]]]; first by rewrite /KP => <-. have [B maxnB sDB]: {B : grT | maxnormal B P P & D \subset B}. by apply: maxgroup_exists; rewrite prDP normal_norm. apply; exists B => //; apply: subnormal_trans snAD (normal_subnormal _). by apply: normalS sDB _ nDP; case/andP: (maxgroupp maxnB); case/andP. have [prBP nBP] := andP (maxgroupp maxnB); have sBP := proper_sub prBP. have{lePm}: #|B| < m by apply: leq_trans (proper_card prBP) _. case/IHm=> {IHm}// [|trnB smnBA]; first by rewrite (pgroupS sBP). have{maxnB} abelPB: is_abelem (P / B). apply: charsimple_solvable (maxnormal_charsimple _ maxnB) _ => //. have [_ ntA _ _] := cstrA; have sAB := subnormal_sub snAB. by apply: mFT_quo_sol; apply: contraL sAB; move/eqP->; rewrite subG1. have{abelPB} [p p_pr pPB]: exists2 p, prime p & p.-group (P / B). by case/is_abelemP: abelPB => p p_pr; case/andP; exists p. have{prBP} pi_p: p \in pi. case/pgroup_pdiv: pPB => [|_ pPB _]. by rewrite -subG1 quotient_sub1 // proper_subn. by apply: pgroupP p_pr pPB; apply: quotient_pgroup. pose S := |/|*(B; q); have p'S: #|S| %% p != 0. have pi'S: pi^'.-nat #|S| := pnat_dvd (atrans_dvd trnB) (pcore_pgroup _ _). by rewrite -prime_coprime // (pnat_coprime _ pi'S) ?pnatE. have{p'S} [Q S_Q nQP]: exists2 Q, Q \in S & P \subset 'N(Q). have sTSB: setT \subset G / B by rewrite -im_quotient quotientS ?subsetT. have modBE: {in P & S, forall x Q, ('JG %% B) Q (coset B x) = 'JG Q x}%act. move=> x Q Px; rewrite inE; move/maxgroupp; case/andP=> _ nQB. by rewrite /= modactE ?(subsetP nBP) ?afixJG ?setTI ?inE. have actsPB: [acts P / B, on S | 'JG %% B \ sTSB]. apply/subsetP=> _ /morphimP[x Nx Px ->]. rewrite !inE; apply/subsetP=> Q S_Q; rewrite inE /= modBE //. by rewrite (actsP (norm_acts_max_norm q B)). move: p'S; rewrite (pgroup_fix_mod pPB actsPB); set nQ := #|_|. case: (posnP nQ) => [->|]; first by rewrite mod0n. rewrite lt0n; case/existsP=> Q /setIP[Q_S fixQ]; exists Q => //. apply/normsP=> x Px; apply: congr_group; have Nx := subsetP nBP x Px. by have:= afixP fixQ (coset B x); rewrite /= modBE ?mem_morphim //= => ->. have [qQ _]:= mem_max_normed S_Q. have{qQ nQP} [Q0 maxQ0 sQQ0] := max_normed_exists qQ nQP. have [_ nQ0P]:= mem_max_normed maxQ0. have actsKmnP: [acts 'O_pi^'('C(P)), on |/|*(P; q) | 'JG]. by rewrite (subset_trans _ (norm_acts_max_norm q P)) // cents_norm ?pcore_sub. case nt_mnP: (1%G \in |/|*(P; q)) => [|{Q S_Q sQQ0}]. rewrite atrans_acts_card actsKmnP trivg_max_norm // imset_set1 in maxQ0 *. have <-: Q = 1%G by apply/trivGP; rewrite -(congr_group (set1P maxQ0)). by rewrite cards1 sub1set (subsetP smnBA). have sAB := subnormal_sub snAB; have sAP := subset_trans sAB sBP. have smnP_S: |/|*(P; q) \subset S. apply/subsetP=> Q1 maxQ1; have [qQ1 nQ1P] := mem_max_normed maxQ1. have ntQ1: Q1 != 1%G by case: eqP nt_mnP maxQ1 => // -> ->. have prNQ1: 'N(Q1) \proper G := mFT_norm_proper ntQ1 (mFT_pgroup_proper qQ1). have nQ1A: A \subset 'N(Q1) := subset_trans sAP nQ1P. have [Q2 maxQ2 sQ12] := max_normed_exists qQ1 (subset_trans sBP nQ1P). have [qQ2 nQ2B] := mem_max_normed maxQ2; apply: etrans maxQ2; congr in_mem. apply: val_inj; suffices: q.-Sylow(Q2) Q1 by move/pHall_id=> /= ->. have qNQ2: q.-group 'N_Q2(Q1) by rewrite (pgroupS _ qQ2) ?subsetIl. pose KN := 'O_pi^'('N(Q1)); have sNQ2_KN: 'N_Q2(Q1) \subset KN. rewrite hyp71 // inE normsI ?norms_norm ?(subset_trans sAB nQ2B) //=. by rewrite /psubgroup subsetIr andbT; apply: pi_pnat qNQ2 _. rewrite -Sylow_subnorm (pHall_subl _ sNQ2_KN) ?subsetI ?sQ12 ?normG //= -/KN. suff: exists Q3 : grT, [/\ q.-Sylow(KN) Q3, P \subset 'N(Q3) & Q1 \subset Q3]. move: maxQ1; rewrite inE; case/maxgroupP=> _ maxQ1 [Q3 [sylQ3 nQ3P sQ13]]. by rewrite -(maxQ1 Q3) // (pHall_pgroup sylQ3). apply: coprime_Hall_subset; rewrite //= -/KN. - by rewrite gFnorm_trans ?norms_norm. - by rewrite coprime_sym (pnat_coprime piP (pcore_pgroup _ _)). - by rewrite (solvableS (pcore_sub _ _)) ?mFT_sol. by rewrite pcore_max ?normalG // /pgroup (pi_pnat qQ1). split; last exact: subset_trans smnP_S smnBA. apply/imsetP; exists Q0 => //; apply/setP=> Q2. apply/idP/imsetP=> [maxQ2 | [k Pk ->]]; last by rewrite (actsP actsKmnP). have [S_Q0 S_Q2]: Q0 \in S /\ Q2 \in S by rewrite !(subsetP smnP_S). pose KB := 'O_pi^'('C(B)); pose KBP := KB <*> P. have pi'KB: pi^'.-group KB by apply: pcore_pgroup. have nKB_P: P \subset 'N(KB) by rewrite gFnorm_trans ?norms_cent. have [k KBk defQ2]:= atransP2 trnB S_Q0 S_Q2. have [qQ2 nQ2P] := mem_max_normed maxQ2. have hallP: pi.-Hall('N_KBP(Q2)) P. have sPN: P \subset 'N_KBP(Q2) by rewrite subsetI joing_subr. rewrite pHallE eqn_leq -{1}(part_pnat_id piP) dvdn_leq ?partn_dvd ?cardSg //. have ->: #|P| = #|KBP|`_pi. rewrite /KBP joingC norm_joinEl // coprime_cardMg ?(pnat_coprime piP) //. by rewrite partnM // part_pnat_id // part_p'nat // muln1. by rewrite sPN dvdn_leq ?partn_dvd ?cardSg ?cardG_gt0 ?subsetIl. have hallPk: pi.-Hall('N_KBP(Q2)) (P :^ k). rewrite pHallE -(card_Hall hallP) cardJg eqxx andbT subsetI /=. by rewrite defQ2 normJ conjSg conj_subG ?joing_subr // mem_gen // inE KBk. have [gz]: exists2 gz, gz \in 'N_KBP(Q2) & P :=: (P :^ k) :^ gz. apply: Hall_trans (solvableS (subsetIr _ _) _) hallP hallPk. have ntQ2: Q2 != 1%G by case: eqP nt_mnP maxQ2 => // -> ->. exact: mFT_sol (mFT_norm_proper ntQ2 (mFT_pgroup_proper qQ2)). rewrite [KBP]norm_joinEr //= setIC -group_modr //= setIC -/KB. case/imset2P=> g z; case/setIP=> KBg nQ2g Pz ->{gz} defP. exists (k * g); last first. by apply: val_inj; rewrite /= conjsgM -(normP nQ2g) defQ2. rewrite /KP -defK // (subsetP (subsetIl _ 'C(B))) //= setIAC defK // -/KB. rewrite -coprime_norm_cent 1?coprime_sym ?(pnat_coprime piP) //= -/KB. rewrite inE groupM //; apply/normP. by rewrite -{2}(conjsgK z P) (conjGid Pz) {2}defP /= !conjsgM conjsgK. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div choice fintype bigop) mathcomp(finset prime fingroup morphism automorphism action quotient) mathcomp(gfunctor cyclic pgroup center commutator gseries nilpotent) mathcomp(sylow abelian maximal hall) odd_order(BGsection1 BGsection6)