proposition: Theorem Fcore_structure M (Ms := M`_\sigma) : M \in 'M -> [/\ M`_\F != 1, M`_\F \subset Ms, Ms \subset M^`(1) & M^`(1) \proper M] /\ (forall K D : {group gT}, \kappa(M).-Hall(M) K -> M`_\F != M`_\sigma -> let p := #|K| in let Ks := 'C_Ms(K) in let q := #|Ks| in let Q := 'O_q(M) in let Q0 := 'C_Q(D) in let Qbar := Q / Q0 in q^'.-Hall(M`_\sigma) D -> [/\ [/\ M \in 'M_'P1, Ms ><| K = M & Ms = M ^`(1)], [/\ prime p, prime q, q \in \pi(M`_\F) & q \in \beta(M)], [/\ q.-Sylow(M) Q, nilpotent D & Q0 <| M], [/\ minnormal Qbar (M / Q0), q.-abelem Qbar & #|Qbar| = (q ^ p)%N] & [/\ Ms^`(1) = M^`(2), M^`(2) \subset 'F(M), [/\ Q <*> 'C_M(Q) = 'F(M), 'C_M(Qbar | 'Q) = 'F(M) & 'C_Ms (Ks / Q0 | 'Q) = 'F(M)] & 'F(M) \proper Ms]]).
proof: Proof. move=> maxM; set M' := M^`(1); set M'' := M^`(2). have nsMsM: Ms <| M := pcore_normal _ M; have [sMsM nMsM] := andP nsMsM. have solM := mmax_sol maxM; have solMs: solvable Ms := solvableS sMsM solM. have sMF_Ms: M`_\F \subset Ms := Fcore_sub_Msigma maxM. have ltM'M: M' \proper M by rewrite (sol_der1_proper solM) ?mmax_neq1. have sMsM': Ms \subset M' := Msigma_der1 maxM. have [-> | ltMF_Ms] := eqVproper sMF_Ms; first by rewrite eqxx Msigma_neq1. set KDpart := (X in _ /\ X); suffices KD_holds: KDpart. do 2!split=> //; have [K hallK] := Hall_exists \kappa(M) solM. pose q := #|'C_(M`_\sigma)(K)|; have [D hallD] := Hall_exists q^' solMs. have [_ [_ _ piMFq _] _ _ _] := KD_holds K D hallK (proper_neq ltMF_Ms) hallD. by rewrite -rank_gt0 (leq_trans _ (p_rank_le_rank q _)) ?p_rank_gt0. move=> {KDpart} K D hallK neMF_Ms p Ks q Q /= hallD. have not_nilMs: ~~ nilpotent Ms by rewrite (sameP (Fcore_eq_Msigma maxM) eqP). have P1maxM: M \in 'M_'P1; last have [PmaxM _] := setIdP P1maxM. apply: contraR not_nilMs => notP1maxM; apply: notP1type_Msigma_nil. by rewrite orbC inE notP1maxM inE maxM andbT orNb. have ntK: K :!=: 1 by rewrite inE maxM andbT -(trivg_kappa maxM hallK) in PmaxM. have [defMs defM]: Ms = M' /\ Ms ><| K = M. have [U complU] := ex_kappa_compl maxM hallK. have U1: U :=: 1 by apply/eqP; rewrite (trivg_kappa_compl maxM complU). have [[defM _ _] [//| defM' _] _ _ _] := kappa_structure maxM complU. by rewrite U1 sdprodg1 in defM defM'. have [_ mulMsK nMsK _] := sdprodP defM; rewrite /= -/Ms in mulMsK nMsK. have [sKM kK _] := and3P hallK; have s'K := sub_pgroup (@kappa_sigma' _ _) kK. have coMsK: coprime #|Ms| #|K| := pnat_coprime (pcore_pgroup _ _) s'K. have q_pr: prime q. have [L _ [_ _ _ _ [_]]] := Ptype_embedding PmaxM hallK. by rewrite inE P1maxM => [[] []]. have hallMs: \sigma(M).-Hall(M) Ms := Msigma_Hall maxM. have sMq: q \in \sigma(M). by rewrite -pnatE // -pgroupE (pgroupS (subsetIl _ _) (pcore_pgroup _ _)). have{s'K kK} q'K: q^'.-group K := pi'_p'group s'K sMq. have nsQM: Q <| M := pcore_normal q M; have [sQM nQM] := andP nsQM. have qQ: q.-group Q := pcore_pgroup _ _. have sQMs: Q \subset Ms by rewrite (sub_Hall_pcore hallMs) ?(pi_pgroup qQ). have [K1 prK1 sK1K]: exists2 K1, prime #|gval K1| & K1 \subset K. have:= ntK; rewrite -rank_gt0; have [r r_pr ->] := rank_witness K. by case/p_rank_geP=> K1 /pnElemPcard[? _ oK1]; exists K1; rewrite ?oK1. have coMsK1 := coprimegS sK1K coMsK; have coQK1 := coprimeSg sQMs coMsK1. have prMsK: semiprime Ms K by have [[? _ []] ] := Ptype_structure PmaxM hallK. have defCMsK1: 'C_Ms(K1) = Ks. by rewrite (cent_semiprime prMsK) // -cardG_gt1 prime_gt1. have sK1M := subset_trans sK1K sKM; have nQK1 := subset_trans sK1M nQM. have{sMsM'} sKsQ: Ks \subset Q. have defMsK: [~: Ms, K] = Ms by case/coprime_der1_sdprod: defM. have hallQ := nilpotent_pcore_Hall q (Fitting_nil M). rewrite -[Q]p_core_Fitting (sub_Hall_pcore hallQ) //; first exact: pnat_id. apply: prime_meetG => //; apply: contraNneq not_nilMs => tiKsFM. suffices <-: 'F(Ms) = Ms by apply: Fitting_nil. apply/eqP; rewrite eqEsubset Fitting_sub /= -{1}defMsK. rewrite (odd_sdprod_primact_commg_sub_Fitting defM) ?mFT_odd //. apply/trivgP; rewrite -tiKsFM setIAC setSI //= -/Ms subsetI Fitting_sub /=. by rewrite Fitting_max ?Fitting_nil // gFnormal_trans. have nilMs_Q: nilpotent (Ms / Q). have [nMsK1 tiQK1] := (subset_trans sK1K nMsK, coprime_TIg coQK1). have prK1b: prime #|K1 / Q| by rewrite -(card_isog (quotient_isog _ _)). have defMsK1: (Ms / Q) ><| (K1 / Q) = (Ms / Q) <*> (K1 / Q). by rewrite sdprodEY ?quotient_norms // coprime_TIg ?coprime_morph. apply: (prime_Frobenius_sol_kernel_nil defMsK1) => //. by rewrite (solvableS _ (quotient_sol _ solM)) ?join_subG ?quotientS. by rewrite -coprime_quotient_cent ?quotientS1 /= ?defCMsK1. have defQ: 'O_q(Ms) = Q by rewrite -(setIidPl sQMs) pcore_setI_normal. have sylQ: q.-Sylow(Ms) Q. have nsQMs: Q <| Ms by rewrite -defQ pcore_normal. rewrite -(pquotient_pHall qQ) // /= -/Q -{3}defQ. by rewrite -(pquotient_pcore _ qQ) ?nilpotent_pcore_Hall. have{sMq hallMs} sylQ_M := subHall_Sylow hallMs sMq sylQ. have sQ_MF: Q \subset M`_\F. by rewrite sub_gen ?(bigcup_max [group of Q]) ?(p_Sylow sylQ_M) ?pcore_normal. have{sQ_MF} piMFq: q \in \pi(M`_\F). by rewrite (piSg sQ_MF) // (piSg sKsQ) // pi_of_prime ?inE /=. without loss nDK: D hallD / K \subset 'N(D). have [E hallE nEK] := coprime_Hall_exists q^' nMsK coMsK solMs. have [x Ms_x ->] := Hall_trans solMs hallD hallE. set Q0 := 'C__(_)%G; rewrite -(isog_nil (conj_isog _ _)) -['C_Q(_)]/(gval Q0). move/(_ E hallE nEK)=> IH; suffices ->: Q0 = [group of 'C_Q(E)] by []. apply: group_inj => /=; have Mx: x \in M := subsetP (pcore_sub _ _) x Ms_x. rewrite /= -/Q -{1}(normsP nQM x Mx) centJ -conjIg (normsP _ x Mx) //. by case: IH => _ _ [_ _]; case/andP. set Q0 := 'C_Q(D); set Qb := Q / Q0. have defQD: Q ><| D = Ms by rewrite -defQ in sylQ *; apply/sdprod_Hall_pcoreP. have [_ mulQD nQD tiQD] := sdprodP defQD; rewrite /= -/Q -/Ms in mulQD nQD tiQD. have nilD: nilpotent D. by rewrite (isog_nil (quotient_isog nQD tiQD)) /= -quotientMidl mulQD. have [sDMs q'D _] := and3P hallD; have sDM := subset_trans sDMs sMsM. have sDKM: D <*> K \subset M by rewrite join_subG sDM. have q'DK: q^'.-group (D <*> K) by rewrite norm_joinEr // pgroupM q'D. have{K1 sK1M sK1K coMsK1 coQK1 prK1 defCMsK1 nQK1 solMs} Qi_rec Qi: Qi \in |/|_Q(D <*> K; q) -> Q0 \subset Qi -> Qi \proper Q -> exists L, [/\ L \in |/|_Q(D <*> K; q), Qi <| L, minnormal (L / Qi) (M / Qi) & ~~ ((Ks \subset L) ==> (Ks \subset Qi))]. - case/setIdP=> /andP[sQiQ qQi] nQiDK sQ0i ltQiQ. have ltQiN := nilpotent_proper_norm (pgroup_nil qQ) ltQiQ. have [Lb minLb sLbQ]: {Lb | minnormal (gval Lb) (M / Qi) & Lb \subset Q / Qi}. apply: mingroup_exists; rewrite quotient_norms //= andbT -quotientInorm. by rewrite -subG1 quotient_sub1 ?subsetIr // proper_subn. have [ntLb nLbM] := andP (mingroupp minLb). have nsQiN: Qi <| 'N_M(Qi) by rewrite normal_subnorm (subset_trans sQiQ). have: Lb <| 'N_M(Qi) / Qi. by rewrite quotientInorm /normal (subset_trans sLbQ) ?quotientS. case/(inv_quotientN nsQiN) => L defLb sQij /=; case/andP. case/subsetIP=> sLM nQij nLN; exists L. have{sLbQ} sLQ: L \subset Q by rewrite -(quotientSGK nQij sQiQ) -defLb. rewrite inE /psubgroup /normal sLQ sQij nQij (pgroupS sLQ qQ) -defLb. have nLDK: D <*> K \subset 'N(L) by apply: subset_trans nLN; apply/subsetIP. have sLD_Ms: L <*> D \subset Ms by rewrite join_subG (subset_trans sLQ). have coLD_K1: coprime #|L <*> D| #|K1| := coprimeSg sLD_Ms coMsK1. have [[nQiD nQiK] [nLD nLK]] := (joing_subP nQiDK, joing_subP nLDK). have [nQiK1 nLK1] := (subset_trans sK1K nQiK, subset_trans sK1K nLK). split=> //; apply: contra ntLb => regLK. have [sLLD sDLD] := joing_subP (subxx (L <*> D)). suffices nilLDbar: nilpotent (L <*> D / Qi). rewrite defLb -subG1 -(quotientS1 sQ0i) /= -/Q. rewrite coprime_quotient_cent ?(pgroup_sol qQ) ?(pnat_coprime qQ) //=. rewrite subsetI quotientS //= (sub_nilpotent_cent2 nilLDbar) ?quotientS //. by rewrite coprime_morph ?(p'nat_coprime q'D (pgroupS sLQ qQ)). have defLK1b: (L <*> D / Qi) ><| (K1 / Qi) = (L <*> D / Qi) <*> (K1 / Qi). rewrite sdprodEY ?coprime_TIg ?quotient_norms //=. by rewrite (subset_trans sK1K) // normsY. by rewrite coprime_morph // (coprimeSg sLD_Ms). have [sQiLD sLD_M] := (subset_trans sQij sLLD, subset_trans sLD_Ms sMsM). have{regLK}: 'C_(L <*> D / Qi)(K1 / Qi) = 1. rewrite -coprime_quotient_cent ?(subset_trans sK1K) ?(solvableS sLD_M) //=. rewrite -(setIidPr sLD_Ms) setIAC defCMsK1 quotientS1 //= -/Ks joingC. rewrite norm_joinEl // -(setIidPl sKsQ) -setIA -group_modr // tiQD mul1g. have [-> | ntLKs] := eqVneq (Ks :&: L) 1; first exact: sub1G. by rewrite subIset ?(implyP regLK) // prime_meetG. apply: (prime_Frobenius_sol_kernel_nil defLK1b). by apply: solvableS (quotient_sol _ solM); rewrite join_subG !quotientS. by rewrite -(card_isog (quotient_isog _ _)) ?coprime_TIg // (coprimeSg sQiQ). have ltQ0Q: Q0 \proper Q. rewrite properEneq subsetIl andbT; apply: contraNneq not_nilMs => defQ0. rewrite -dprodEsd // in defQD; last by rewrite centsC -defQ0 subsetIr. by rewrite (dprod_nil defQD) (pgroup_nil qQ). have [nQK coQK] := (subset_trans sKM nQM, pnat_coprime qQ q'K). have solQ := pgroup_sol qQ. have [coDK coQD] := (coprimeSg sDMs coMsK, pnat_coprime qQ q'D). have nQ0K: K \subset 'N(Q0) by rewrite normsI ?norms_cent. have nQ0D: D \subset 'N(Q0) by rewrite cents_norm // centsC subsetIr. have nQ0DK: D <*> K \subset 'N(Q0) by apply/joing_subP. have [|Q1 [DKinvQ1 nsQ01 minQ1b nregQ1b]] := Qi_rec _ _ (subxx _) ltQ0Q. by rewrite inE /psubgroup (pgroupS _ qQ) ?subsetIl. have{Qi_rec nregQ1b DKinvQ1} [tiQ0Ks defQ1]: Q0 :&: Ks = 1 /\ Q1 :=: Q. move: nregQ1b; rewrite negb_imply; case/andP=> sKsQ1 not_sKsQ0. split=> //; first by rewrite setIC prime_TIg. have [] := setIdP DKinvQ1; case/andP; case/eqVproper=> // ltQ1Q _ _. have [Q2 [_ _ _]] := Qi_rec Q1 DKinvQ1 (normal_sub nsQ01) ltQ1Q. by rewrite sKsQ1 implybT. have [nsQ0Q minQb]: Q0 <| Q /\ minnormal Qb (M / Q0) by rewrite /Qb -defQ1. have{Q1 defQ1 minQ1b nsQ01} abelQb: q.-abelem Qb. have qQb: q.-group Qb := quotient_pgroup _ qQ; have solQb := pgroup_sol qQb. by rewrite -is_abelem_pgroup // (minnormal_solvable_abelem minQb). have [cQbQb [sQ0Q nQ0Q]] := (abelem_abelian abelQb, andP nsQ0Q). have nQ0M: M \subset 'N(Q0) by rewrite -mulMsK -mulQD -mulgA !mul_subG. have nsQ0M: Q0 <| M by rewrite /normal subIset ?sQM. have sFM_QCQ: 'F(M) \subset Q <*> 'C_M(Q). have [_ /= mulQQ' cQQ' _] := dprodP (nilpotent_pcoreC q (Fitting_nil M)). rewrite -{3}mulQQ' p_core_Fitting cent_joinEr ?subsetIr //= -/Q in cQQ' *. by rewrite mulgS // subsetI gFsub_trans ?gFsub. have sQCQ_CMsQb: Q <*> 'C_M(Q) \subset 'C_Ms(Qb | 'Q). rewrite join_subG !(subsetI _ Ms) sQMs /= !sub_astabQ nQ0Q /= -/Q0 -/Qb. rewrite -abelianE cQbQb quotient_cents ?subsetIr //= andbC subIset ?nQ0M //=. rewrite -(coprime_mulG_setI_norm mulMsK) ?norms_cent //= -/Ms. suffices ->: 'C_K(Q) = 1 by rewrite mulg1 subsetIl. have: ~~ (Q \subset Ks); last apply: contraNeq => ntCKQ. have [_ _ _ [_]] := Ptype_structure PmaxM hallK. by move/(_ q); rewrite pi_of_prime //; case/(_ (eqxx q) _ sylQ_M). rewrite -[Ks](cent_semiprime prMsK _ ntCKQ) ?subsetIl //. by rewrite subsetI sQMs centsC subsetIr. have nCQb: M \subset 'N('C(Qb | 'Q)). by rewrite (subset_trans _ (astab_norm _ _)) ?actsQ. have defFM: 'C_Ms(Qb | 'Q) = 'F(M). apply/eqP; rewrite eqEsubset andbC (subset_trans sFM_QCQ) //=. rewrite Fitting_max //=; first by rewrite /normal subIset ?sMsM //= normsI. rewrite -(coprime_mulG_setI_norm mulQD) ?(subset_trans sMsM) //= -/Q. rewrite mulg_nil ?(nilpotentS (subsetIl _ _)) ?(pgroup_nil qQ) //= -/Q. rewrite (centsS (subsetIl _ _)) //= -/Q. have cDQ0: 'C_D(Qb | 'Q) \subset 'C(Q0) by rewrite subIset // centsC subsetIr. rewrite (stable_factor_cent cDQ0) ?(coprimegS (subsetIl _ _) coQD) //. by rewrite /stable_factor commGC -sub_astabQR ?subsetIr // subIset ?nQ0D. have{sFM_QCQ sQCQ_CMsQb} ->: Q <*> 'C_M(Q) = 'F(M). by apply/eqP; rewrite eqEsubset sFM_QCQ andbT -defFM. have ltFM_Ms: 'F(M) \proper Ms. rewrite properEneq -{2}defFM subsetIl andbT. by apply: contraNneq not_nilMs => <-; apply: Fitting_nil. have sQFM: Q \subset 'F(M) by rewrite -[Q]p_core_Fitting pcore_sub. have not_cDQb: ~~ (D / Q0 \subset 'C(Qb)). apply: contra (proper_subn ltFM_Ms) => cDQb; rewrite -mulQD mulG_subG sQFM /=. by rewrite -defFM subsetI sDMs sub_astabQ nQ0D. have [_ minQbP] := mingroupP minQb. have regQbDb: 'C_Qb(D / Q0) = 1. apply: contraNeq not_cDQb => ntCQDb; rewrite centsC; apply/setIidPl. apply: minQbP (subsetIl _ _); rewrite ntCQDb /= -/Qb -(setIidPl cQbQb) -setIA. by rewrite -centM -quotientMl //= mulQD normsI ?norms_cent ?quotient_norms. have tiQ0 R: q^'.-group R -> Q0 :&: R = 1. by move/(pnat_coprime (pgroupS sQ0Q qQ))/coprime_TIg. have oKb: #|K / Q0| = p by rewrite -(card_isog (quotient_isog _ (tiQ0 _ _))). have oKsb: #|Ks / Q0| = q. by rewrite -(card_isog (quotient_isog _ tiQ0Ks)) ?(subset_trans sKsQ). have regDK: 'C_D(K) = 1. by rewrite -(setIidPl sDMs) -setIA setIC coprime_TIg ?(coprimeSg sKsQ). have{tiQ0} frobDKb: [Frobenius D <*> K / Q0 = (D / Q0) ><| (K / Q0)]. have ntDb: D / Q0 != 1 by apply: contraNneq not_cDQb => ->; apply: sub1G. have ntKb: K / Q0 != 1 by rewrite -(isog_eq1 (quotient_isog _ (tiQ0 _ _))). apply/Frobenius_semiregularP => // [|xb]. by apply: quotient_coprime_sdprod; rewrite ?sdprodEY ?coprime_TIg. have [f [_ ker_f _ im_f]] := restrmP (coset_morphism Q0) nQ0DK. have{ker_f} inj_f: 'injm f by rewrite ker_f ker_coset setIC tiQ0. rewrite /= /quotient -!im_f ?joing_subl ?joing_subr //. rewrite 2!inE andbC => /andP[/morphimP[x DKx Kx ->{xb}]]. rewrite morph_injm_eq1 // -injm_subcent1 ?joing_subl // => ntx. rewrite -{3}(setIidPl sDMs) -setIA prMsK ?inE ?ntx //. by rewrite setICA regDK setIg1 morphim1. have defKsb: 'C_Qb(K / Q0) = Ks / Q0. rewrite /Ks -mulQD coprime_cent_mulG // regDK mulg1. by rewrite coprime_quotient_cent ?subsetIl. have{frobDKb regQbDb} [p_pr oQb cQbD']: [/\ prime p, #|Qb| = (q ^ p)%N & (D / Q0)^`(1) \subset 'C(Qb)]. - have ntQb: Qb != 1 by rewrite -subG1 quotient_sub1 ?proper_subn. have prQbK: semiprime Qb (K / Q0). move=> xb; rewrite 2!inE andbC; case/andP; case/morphimP=> x nQ0x Kx -> ntx. have{} ntx: x != 1 by apply: contraNneq ntx => ->; rewrite morph1. transitivity ('C_Q[x] / Q0); last first. rewrite -(coprime_quotient_cent (subsetIl Q _) nQ0K coQK solQ) /= -/Q0. by rewrite -/Q -(setIidPl sQMs) -!setIA prMsK // !inE ntx. rewrite -!cent_cycle -quotient_cycle //; rewrite -!cycle_subG in Kx nQ0x. by rewrite coprime_quotient_cent ?(coprimegS Kx). have:= Frobenius_primact frobDKb _ _ _ ntQb _ prQbK regQbDb. have [nQDK solDK] := (subset_trans sDKM nQM, solvableS sDKM solM). rewrite !quotient_sol ?quotient_norms // coprime_morph ?(pnat_coprime qQ) //=. rewrite -/Qb oKb defKsb prime_cyclic oKsb // subsetI der_sub /=. by case=> //= -> -> ->. have{cQbD'} sM''FM: M'' \subset 'F(M). have nQMs := subset_trans sMsM nQM. rewrite [M'']dergSn -/M' -defMs -(quotientSGK _ sQFM) ?comm_subG //. rewrite (quotient_der 1) //= -/Ms -mulQD quotientMidl -quotient_der //= -/Q. by rewrite quotientS // -defFM subsetI sub_astabQ !comm_subG ?quotient_der. have sQ0Ms := subset_trans sQ0Q sQMs. have ->: 'C_Ms(Ks / Q0 | 'Q) = 'F(M). have sFMcKsb: 'F(M) \subset 'C_Ms(Ks / Q0 | 'Q). by rewrite -defFM setIS ?astabS ?quotientS. have nCMsKsbM: M \subset 'N('C_Ms(Ks / Q0 | 'Q)). rewrite -{1}mulMsK mulG_subG sub_der1_norm ?subsetIl //= -/Ms; last first. by rewrite {1}defMs (subset_trans sM''FM sFMcKsb). rewrite normsI // (subset_trans _ (astab_norm _ _)) ?actsQ //. by rewrite cents_norm // centsC subsetIr. apply/eqP; rewrite eqEsubset sFMcKsb -defFM subsetI subsetIl. rewrite sub_astabQ /= -/Q0 subIset ?(subset_trans sMsM) //= andbT centsC. apply/setIidPl; apply: minQbP (subsetIl _ _). rewrite andbC normsI ?norms_cent ?quotient_norms //= -/Qb. have: Ks / Q0 != 1 by rewrite -cardG_gt1 oKsb prime_gt1. apply: subG1_contra; rewrite (quotientGI _ sQ0Ms) quotient_astabQ /= -/Q0. by rewrite subsetI quotientS // centsC subsetIr. have ->: 'C_M(Qb | 'Q) = 'F(M). apply/eqP; rewrite eqEsubset -{2}defFM setSI //= andbT. rewrite -(coprime_mulG_setI_norm mulMsK) //= -defFM mulG_subG subxx /=. rewrite subsetI subsetIr -(quotientSGK _ sQ0Ms) 1?subIset ?nQ0K //= -/Q0. rewrite quotientIG; last by rewrite sub_astabQ normG trivg_quotient sub1G. rewrite quotient_astabQ /= -/Q0 prime_TIg ?sub1G ?oKb //. rewrite centsC -subsetIidl defKsb; apply: contra (@subset_leq_card _ _ _) _. by rewrite -ltnNge oQb oKsb (ltn_exp2l 1) prime_gt1. suffices ->: q \in \beta(M) by do 2!split=> //; last rewrite {1}defMs. apply: contraR not_cDQb; rewrite negb_forall_in; case/exists_inP=> Q1 sylQ1. rewrite negbK {Q1 sylQ1}(eq_Hall_pcore sylQ_M sylQ1) -/Q => nnQ. have sD_DK': D \subset (D <*> K)^`(1). rewrite -{1}(coprime_cent_prod nDK) ?nilpotent_sol // regDK mulg1. by rewrite commgSS ?joing_subl ?joing_subr. rewrite quotient_cents // (subset_trans sD_DK') //. have nQDK := subset_trans sDKM nQM; have nCQDK := norms_cent nQDK. rewrite der1_min // -(isog_abelian (second_isog nCQDK)) setIC /=. rewrite -ker_conj_aut (isog_abelian (first_isog_loc _ _)) //=; set A := _ @* _. have norm_q := normal_norm (pcore_normal q _). rewrite {norm_q}(isog_abelian (quotient_isog (norm_q _ _) _)) /=; last first. by rewrite coprime_TIg ?coprime_morphr //= (pnat_coprime (pcore_pgroup q _)). have AutA: A \subset [Aut Q] := Aut_conj_aut _ _. have [|//] := Aut_narrow qQ (mFT_odd _) nnQ _ AutA (morphim_odd _ (mFT_odd _)). exact: morphim_sol (solvableS sDKM solM). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq choice div fintype) mathcomp(path bigop finset prime fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor pgroup cyclic commutator) mathcomp(center gseries nilpotent sylow abelian maximal hall frobenius) odd_order(BGsection1 BGsection2 BGsection3 BGsection4 BGsection5) odd_order(BGsection6 BGsection7 BGsection9 BGsection10 BGsection12) odd_order(BGsection13 BGsection14)