proposition: Theorem odd_sdprod_primact_commg_sub_Fitting gT (G K R : {group gT}) : K ><| R = G -> odd #|G| -> solvable G -> coprime #|K| #|R| -> semiprime K R -> 'C_('F(K))(R) = 1 -> [~: K, R] \subset 'F(K).
proof: Proof. elim: {G}_.+1 {-2}G (ltnSn #|G|) K R => // n IHn G. rewrite ltnS => leGn K R defG oddG solG coKR primR regR_F. have [nsKG sRG defKR nKR tiKR] := sdprod_context defG. have [sKG nKG] := andP nsKG. have chF: 'F(K) \char K := Fitting_char K; have nFR := char_norm_trans chF nKR. have nsFK := char_normal chF; have [sFK nFK] := andP nsFK. pose KqF := K / 'F(K); have solK := solvableS sKG solG. without loss [p p_pr pKqF]: / exists2 p, prime p & p.-group KqF. move=> IHp; apply: wlog_neg => IH_KR; rewrite -quotient_cents2 //= -/KqF. set Rq := R / 'F(K); have nKRq: Rq \subset 'N(KqF) by apply: quotient_norms. rewrite centsC. apply: subset_trans (coprime_cent_Fitting nKRq _ _); last first. - exact: quotient_sol. - exact: coprime_morph. rewrite subsetI subxx centsC -['F(KqF)]Sylow_gen gen_subG. apply/bigcupsP=> Pq /SylowP[p p_pr /= sylPq]; rewrite -/KqF in sylPq. have chPq: Pq \char KqF. apply: char_trans (Fitting_char _); rewrite /= -/KqF. by rewrite (nilpotent_Hall_pcore (Fitting_nil _) sylPq) ?pcore_char. have [P defPq sFP sPK] := inv_quotientS nsFK (char_sub chPq). have nsFP: 'F(K) <| P by rewrite /normal sFP (subset_trans sPK). have{chPq} chP: P \char K. by apply: char_from_quotient nsFP (Fitting_char _) _; rewrite -defPq. have defFP: 'F(P) = 'F(K). apply/eqP; rewrite eqEsubset !Fitting_max ?Fitting_nil //. by rewrite char_normal ?gFchar_trans. have coPR := coprimeSg sPK coKR. have nPR: R \subset 'N(P) := char_norm_trans chP nKR. pose G1 := P <*> R. have sG1G: G1 \subset G by rewrite /G1 -defKR norm_joinEr ?mulSg. have defG1: P ><| R = G1 by rewrite sdprodEY ?coprime_TIg. rewrite defPq quotient_cents2r //= -defFP. have:= sPK; rewrite subEproper; case/predU1P=> [defP | ltPK]. rewrite IHp // in IH_KR; exists p => //. by rewrite /KqF -{2}defP -defPq (pHall_pgroup sylPq). move/IHn: defG1 => ->; rewrite ?(oddSg sG1G) ?(solvableS sG1G) ?defFP //. apply: leq_trans leGn; rewrite /= norm_joinEr //. by rewrite -defKR !coprime_cardMg // ltn_pmul2r ?proper_card. by move=> x Rx; rewrite -(setIidPl sPK) -!setIA primR. without loss r_pr: / prime #|R|; last set r := #|R| in r_pr. have [-> _ | [r r_pr]] := trivgVpdiv R; first by rewrite commG1 sub1G. case/Cauchy=> // x; rewrite -cycle_subG subEproper orderE; set X := <[x]>. case/predU1P=> [-> -> -> // | ltXR rX _]; have sXR := proper_sub ltXR. have defCX: 'C_K(X) = 'C_K(R). rewrite cent_cycle primR // !inE -order_gt1 orderE rX prime_gt1 //=. by rewrite -cycle_subG. have primX: semiprime K X. by move=> y; case/setD1P=> nty Xy; rewrite primR // !inE nty (subsetP sXR). have nKX := subset_trans sXR nKR; have coKX := coprimegS sXR coKR. pose H := K <*> X; have defH: K ><| X = H by rewrite sdprodEY ?coprime_TIg. have sHG: H \subset G by rewrite /H -defKR norm_joinEr ?mulgSS. have ltHn: #|H| < n. rewrite (leq_trans _ leGn) /H ?norm_joinEr // -defKR !coprime_cardMg //. by rewrite ltn_pmul2l ?proper_card. have oddH := oddSg sHG oddG; have solH := solvableS sHG solG. have regX_F: 'C_('F(K))(X) = 1. by rewrite -regR_F -(setIidPl sFK) -!setIA defCX. have:= IHn _ ltHn _ _ defH oddH solH coKX primX regX_F. rewrite -!quotient_cents2 ?(subset_trans sXR) //; move/setIidPl <-. rewrite -coprime_quotient_cent ?(subset_trans sXR) // defCX. by rewrite coprime_quotient_cent ?subsetIr. apply: subset_trans (chief_stab_sub_Fitting solG nsKG) => //. rewrite subsetI commg_subl nKR; apply/bigcapsP => [[U V]] /=. case/andP=> chiefUV sUF; set W := U / V. have minW := chief_factor_minnormal chiefUV. have [ntW nWG] := andP (mingroupp minW). have /andP[/maxgroupp/andP[/andP[sVU _] nVG] nsUG] := chiefUV. have sUK := subset_trans sUF sFK; have sVK := subset_trans sVU sUK. have nVK := subset_trans sKG nVG; have nVR := subset_trans sRG nVG. have [q q_pr abelW]: exists2 q, prime q & q.-abelem W. apply/is_abelemP; apply: charsimple_solvable (minnormal_charsimple minW) _. by rewrite quotient_sol // (solvableS sUK). have regR_W: 'C_(W)(R / V) = 1. rewrite -coprime_quotient_cent ?(coprimeSg sUK) ?(solvableS sUK) //. by rewrite -(setIidPl sUF) -setIA regR_F (setIidPr _) ?quotient1 ?sub1G. rewrite sub_astabQ comm_subG ?quotientR //=. have defGv: (K / V) * (R / V) = G / V by rewrite -defKR quotientMl. have oRv: #|R / V| = r. rewrite card_quotient // -indexgI -(setIidPr sVK) setICA setIA tiKR. by rewrite (setIidPl (sub1G _)) indexg1. have defCW: 'C_(G / V)(W) = 'C_(K / V)(W). apply/eqP; rewrite eqEsubset andbC setSI ?quotientS //=. rewrite subsetI subsetIr /= andbT. rewrite -(coprime_mulG_setI_norm defGv) ?coprime_morph ?norms_cent //=. suffices ->: 'C_(R / V)(W) = 1 by rewrite mulg1 subsetIl. apply/trivgP; apply/subsetP=> x; case/setIP=> Rx cWx. apply: contraR ntW => ntx; rewrite -subG1 -regR_W subsetI subxx centsC /= -/W. by apply: contraR ntx; move/prime_TIg <-; rewrite ?oRv // inE Rx. have [P sylP nPR] := coprime_Hall_exists p nKR coKR solK. have [sPK pP _] := and3P sylP. have nVP := subset_trans sPK nVK; have nFP := subset_trans sPK nFK. have sylPv: p.-Sylow(K / V) (P / V) by rewrite quotient_pHall. have defKv: (P / V) * 'C_(G / V)(W) = (K / V). rewrite defCW; apply/eqP; rewrite eqEsubset mulG_subG subsetIl quotientS //=. have sK_PF: K \subset P * 'F(K). rewrite (normC nFP) -quotientSK // subEproper eq_sym eqEcard quotientS //=. by rewrite (card_Hall (quotient_pHall nFP sylP)) part_pnat_id ?leqnn. rewrite (subset_trans (quotientS _ sK_PF)) // quotientMl // mulgS //. rewrite subsetI -quotient_astabQ !quotientS //. by rewrite (subset_trans (Fitting_stab_chief solG nsKG)) ?(bigcap_inf (U, V)). have nW_ := subset_trans (quotientS _ _) nWG; have nWK := nW_ _ sKG. rewrite -quotient_cents2 ?norms_cent ?(nW_ _ sRG) //. have [eq_qp | p'q] := eqVneq q p. apply: subset_trans (sub1G _); rewrite -trivg_quotient quotientS // centsC. apply/setIidPl; case/mingroupP: minW => _; apply; last exact: subsetIl. rewrite andbC normsI ?norms_cent // ?quotient_norms //=. have nsWK: W <| K / V by rewrite /normal quotientS. have sWP: W \subset P / V. by rewrite (normal_sub_max_pgroup (Hall_max sylPv)) -?eq_qp ?abelem_pgroup. rewrite -defKv centM setIA setIAC /=. rewrite ['C_W(_)](setIidPl _); last by rewrite centsC subsetIr. have nilPv: nilpotent (P / V) := pgroup_nil (pHall_pgroup sylPv). rewrite -/W -(setIidPl sWP) -setIA meet_center_nil //. exact: normalS (quotientS V sPK) nsWK. rewrite -defKv -quotientMidr -mulgA mulSGid ?subsetIr // quotientMidr. have sPG := subset_trans sPK sKG. rewrite quotient_cents2 ?norms_cent ?nW_ //= commGC. pose Hv := (P / V) <*> (R / V). have sHGv: Hv \subset G / V by rewrite join_subG !quotientS. have solHv: solvable Hv := solvableS sHGv (quotient_sol V solG). have sPHv: P / V \subset Hv by apply: joing_subl. have nPRv: R / V \subset 'N(P / V) := quotient_norms _ nPR. have coPRv: coprime #|P / V| #|R / V| := coprime_morph _ (coprimeSg sPK coKR). apply: subset_trans (subsetIr (P / V) _). have oHv: #|Hv| = (#|P / V| * #|R / V|)%N. by rewrite /Hv norm_joinEr // coprime_cardMg // oRv. move/(odd_prime_sdprod_abelem_cent1 solHv): (abelW); apply=> //. - exact: oddSg sHGv (quotient_odd _ _). - by rewrite sdprodEY ?quotient_norms // coprime_TIg. - by rewrite oRv. - by rewrite (subset_trans _ nWG) ?join_subG ?quotientS. rewrite /= norm_joinEr // pgroupM /pgroup. rewrite (pi_pnat (quotient_pgroup _ pP)) ?inE 1?eq_sym //=. apply: coprime_p'group (abelem_pgroup abelW) ntW. by rewrite coprime_sym coprime_morph // (coprimeSg sUK). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div) mathcomp(fintype tuple bigop prime binomial finset ssralg fingroup finalg) mathcomp(morphism perm automorphism quotient action commutator gproduct) mathcomp(zmodp cyclic gfunctor center pgroup gseries nilpotent sylow) mathcomp(finmodule abelian frobenius maximal extremal hall) mathcomp(matrix mxalgebra mxrepresentation mxabelem) odd_order(wielandt_fixpoint BGsection1 BGsection2)