proposition: Theorem Frobenius_primact gT (G K R M : {group gT}) : [Frobenius G = K ><| R] -> solvable G -> G \subset 'N(M) -> solvable M -> M :!=: 1 -> coprime #|M| #|G| -> semiprime M R -> 'C_M(K) = 1 -> [/\ prime #|R|, #|M| = (#|'C_M(R)| ^ #|R|)%N & cyclic 'C_M(R) -> K^`(1) \subset 'C_K(M)].
proof: Proof. move: {2}_.+1 (ltnSn #|M|) => n; elim: n => // n IHn in gT G K R M *. rewrite ltnS => leMn frobG solG nMG solM ntM coMG primRM tcKM. case: (Frobenius_Wielandt_fixpoint frobG nMG) => // _ _ /(_ tcKM) oM. have [defG ntK ntR ltKG _]:= Frobenius_context frobG. have Rpr: prime #|R|. have [R1 | [r r_pr]] := trivgVpdiv R; first by case/eqP: ntR. case/Cauchy=> // x Rx ox; pose R0 := <[x]>; pose G0 := K <*> R0. have [_ defKR nKR tiKR] := sdprodP defG. have sR0R: R0 \subset R by rewrite cycle_subG. have sG0G: G0 \subset G by rewrite /G0 -genM_join gen_subG -defKR mulgS. have nKR0 := subset_trans sR0R nKR; have nMG0 := subset_trans sG0G nMG. have ntx: <[x]> != 1 by rewrite cycle_eq1 -order_gt1 ox prime_gt1. have [tcRM | ntcRM] := eqVneq 'C_M(R) 1. by rewrite -cardG_gt1 oM tcRM cards1 exp1n in ntM. have frobG0: [Frobenius G0 = K ><| R0]. apply/Frobenius_semiregularP=> // [|y /setD1P[nty x_y]]. by apply: sdprodEY nKR0 (trivgP _); rewrite -tiKR setIS. by apply: (Frobenius_reg_ker frobG); rewrite !inE nty (subsetP sR0R). case: (Frobenius_Wielandt_fixpoint frobG0 nMG0 (coprimegS _ coMG)) => // _ _. move/(_ tcKM)/eqP; rewrite oM cent_cycle. rewrite primRM; last by rewrite !inE Rx andbT -cycle_eq1. by rewrite eqn_exp2l ?cardG_gt1 // -orderE ox => /eqP->. split=> // cyc_cMR. have nM_MG: M <*> G \subset 'N(M) by rewrite join_subG normG. have [V minV sVM] := minnormal_exists ntM nM_MG. have [] := minnormal_solvable minV sVM solM. rewrite join_subG; case/andP=> nVM nVG ntV; case/is_abelemP=> [q q_pr abelV]. have coVG := coprimeSg sVM coMG; have solV := solvableS sVM solM. have cVK': K^`(1) \subset 'C_K(V). case: (eqVneq 'C_V(R) 1) => [tcVR | ntcRV]. case: (Frobenius_Wielandt_fixpoint frobG nVG) => // _. by move/(_ tcVR)=> cVK _; rewrite (setIidPl cVK) der_sub. have ocVR: #|'C_V(R)| = q. have [u def_u]: exists u, 'C_V(R) = <[u]>. by apply/cyclicP; apply: cyclicS (setSI _ sVM) cyc_cMR. rewrite def_u -orderE (abelem_order_p abelV) -?cycle_eq1 -?def_u //. by rewrite -cycle_subG -def_u subsetIl. apply: (Frobenius_prime_cent_prime _ defG _ _ abelV) => //. by case/prime_FrobeniusP: frobG. by rewrite (coprime_p'group _ (abelem_pgroup abelV) ntV) // coprime_sym. have cMK': K^`(1) / V \subset 'C_(K / V)(M / V). have [-> | ntMV] := eqVneq (M / V) 1. by rewrite subsetI cents1 quotientS ?der_sub. have coKR := Frobenius_coprime frobG. case/prime_FrobeniusP: frobG => //. case/sdprod_context=> nsKG sRG defKR nKR tiKR regR; have [sKG _] := andP nsKG. have nVK := subset_trans sKG nVG; have nVR := subset_trans sRG nVG. have RVpr: prime #|R / V|. rewrite card_quotient // -indexgI setIC coprime_TIg ?(coprimegS sRG) //. by rewrite indexg1. have frobGV: [Frobenius G / V = (K / V) ><| (R / V)]. apply/prime_FrobeniusP; rewrite // -?cardG_gt1 ?card_quotient //. rewrite -indexgI setIC coprime_TIg ?(coprimegS sKG) //. by rewrite indexg1 cardG_gt1. rewrite -coprime_norm_quotient_cent ?(coprimegS sRG) //= regR quotient1. rewrite -defKR quotientMl // sdprodE ?quotient_norms //. by rewrite coprime_TIg ?coprime_morph. have ltMVn: #|M / V| < n by apply: leq_trans leMn; rewrite ltn_quotient. rewrite quotient_der //; move/IHn: frobGV. case/(_ _ ltMVn); rewrite ?quotient_sol ?quotient_norms ?coprime_morph //. - move=> Vx; case/setD1P=> ntVx; case/morphimP=> x nVx Rx defVx. rewrite defVx /= -cent_cycle -quotient_cycle //; congr 'C__(_ / V). apply/eqP; rewrite eqEsubset cycle_subG Rx /=. apply: contraR ntVx => /(prime_TIg Rpr)/trivgP. by rewrite defVx /= (setIidPr _) cycle_subG // => /set1P->; rewrite morph1. - rewrite -coprime_norm_quotient_cent ?(coprimegS sKG) ?(subset_trans sKG) //. by rewrite tcKM quotient1. move=> _ _ -> //; rewrite -coprime_quotient_cent ?quotient_cyclic //. by rewrite (coprimegS sRG). have{cVK' cMK'} [[sK'K cVK'] [_ cMVK']] := (subsetIP cVK', subsetIP cMK'). have sK'G: K^`(1) \subset G by rewrite (subset_trans sK'K) ?proper_sub. have coMK': coprime #|M| #|K^`(1)| := coprimegS sK'G coMG. rewrite subsetI sK'K (stable_factor_cent cVK') //; apply/and3P; split=> //. by rewrite commGC -quotient_cents2 // (subset_trans sK'G). 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)