proposition: Theorem odd_sdprod_Zgroup_cent_prime_plength1 p gT (G H R R0 : {group gT}) : solvable G -> odd #|G| -> H ><| R = G -> coprime #|H| #|R| -> R0 \subset R -> prime #|R0| -> Zgroup 'C_H(R0) -> p.-length_1 [~: H, R].
proof: Proof. move: {2}_.+1 (ltnSn #|G|) => n; elim: n => // n IHn in gT G H R R0 *. rewrite ltnS; move oR0: #|R0| => r leGn solG oddG defG coHR sR0R r_pr ZgrCHR0. have rR0: r.-group R0 by rewrite /pgroup oR0 pnat_id. have [nsHG sRG mulHR nHR tiHR]:= sdprod_context defG. have [sHG nHG] := andP nsHG; have solH := solvableS sHG solG. have IHsub (H1 R1 : {group gT}): H1 \subset H -> H1 * R1 \subset 'N(H1) -> R0 \subset R1 -> R1 \subset R -> (#|H1| < #|H|) || (#|R1| < #|R|) -> p.-length_1 [~: H1, R1]. - move=> sH1 nH1 sR01 sR1 ltG1; set G1 := H1 <*> R1. have coHR1: coprime #|H1| #|R1| by rewrite (coprimeSg sH1) // (coprimegS sR1). have defG1: H1 ><| R1 = G1. by rewrite sdprodEY ?coprime_TIg ?(subset_trans (mulG_subr H1 R1)). have sG1: G1 \subset G by rewrite join_subG -mulG_subG -mulHR mulgSS. have{ltG1} ltG1n: #|G1| < n. rewrite (leq_trans _ leGn) // -(sdprod_card defG1) -(sdprod_card defG). have leqifS := leqif_geq (subset_leq_card _). rewrite ltn_neqAle !(leqif_mul (leqifS _ _ _ sH1) (leqifS _ _ _ sR1)). by rewrite muln_eq0 !negb_or negb_and -!ltnNge ltG1 -!lt0n !cardG_gt0. apply: IHn defG1 _ sR01 _ _; rewrite ?oR0 ?(solvableS sG1) ?(oddSg sG1) //. exact: ZgroupS (setSI _ sH1) ZgrCHR0. without loss defHR: / [~: H, R] = H; last rewrite defHR. have sHR_H: [~: H, R] \subset H by rewrite commg_subl. have:= sHR_H; rewrite subEproper; case/predU1P=> [-> -> //|ltHR_H _]. rewrite -coprime_commGid // IHsub 1?proper_card //. by apply: subset_trans (commg_norm H R); rewrite norm_joinEr ?mulSg. have{n leGn IHn tiHR} IHquo (X : {group gT}): X :!=: 1 -> X \subset H -> G \subset 'N(X) -> p.-length_1 (H / X). - move=> ntX sXH nXG; have nXH := subset_trans sHG nXG. have nXR := subset_trans sRG nXG; have nXR0 := subset_trans sR0R nXR. rewrite -defHR quotientE morphimR // -!quotientE. have ltGbn: #|G / X| < n. exact: leq_trans (ltn_quotient ntX (subset_trans sXH sHG)) _. have defGb: (H / X) ><| (R / X) = G / X by apply: quotient_coprime_sdprod. have pr_R0b: prime #|R0 / X|. have tiXR0: X :&: R0 = 1 by apply/trivgP; rewrite -tiHR setISS. by rewrite card_quotient // -indexgI setIC tiXR0 indexg1 oR0. have solGb: solvable (G / X) by apply: quotient_sol. have coHRb: coprime #|H / X| #|R / X| by apply: coprime_morph. apply: IHn defGb coHRb _ pr_R0b _; rewrite ?quotientS ?quotient_odd //. by rewrite -coprime_quotient_cent ?(coprimegS sR0R) // morphim_Zgroup. without loss Op'H: / 'O_p^'(H) = 1. have [_ -> // | ntO _] := eqVneq 'O_p^'(H) 1. suffices: p.-length_1 (H / 'O_p^'(H)). by rewrite p'quo_plength1 ?pcore_normal ?pcore_pgroup. apply: IHquo => //; first by rewrite normal_sub ?pcore_normal. by rewrite normal_norm // gFnormal_trans. move defV: 'F(H)%G => V. have charV: V \char H by rewrite -defV Fitting_char. have /andP[sVH nVH]: V <| H := char_normal charV. have nsVG: V <| G := char_normal_trans charV nsHG. have [_ nVG] := andP nsVG; have nVR: R \subset 'N(V) := subset_trans sRG nVG. without loss ntV: / V :!=: 1. by rewrite -defV trivg_Fitting //; case: eqP => [|_] ->; rewrite ?plength1_1. have scVHV: 'C_H(V) \subset V by rewrite -defV cent_sub_Fitting. have{Op'H} defV: 'O_p(H) = V by rewrite -(Fitting_eq_pcore Op'H) -defV. have pV: p.-group V by rewrite -defV pcore_pgroup. have [p_pr p_dv_V _] := pgroup_pdiv pV ntV. have p'r: r != p. rewrite eq_sym -dvdn_prime2 // -prime_coprime // (coprime_dvdl p_dv_V) //. by rewrite -oR0 (coprimegS sR0R) // (coprimeSg sVH). without loss{charV} abelV: / p.-abelem V; last have [_ cVV eV] := and3P abelV. move/implyP; rewrite implybE -trivg_Phi //; case/orP=> // ntPhi. have charPhi: 'Phi(V) \char H := gFchar_trans _ charV. have nsPhiH := char_normal charPhi; have [sPhiH nPhiH] := andP nsPhiH. have{charPhi} nPhiG: G \subset 'N('Phi(V)):= char_norm_trans charPhi nHG. rewrite -(pquo_plength1 nsPhiH) 1?IHquo ?(pgroupS (Phi_sub _)) //. have [/= W defW sPhiW nsWH] := inv_quotientN nsPhiH (pcore_normal p^' _). have p'Wb: p^'.-group (W / 'Phi(V)) by rewrite -defW pcore_pgroup. have{p'Wb} tiWb := coprime_TIg (pnat_coprime (quotient_pgroup _ _) p'Wb). suffices pW: p.-group W by rewrite -(tiWb W pW) setIid. apply/pgroupP=> q q_pr; case/Cauchy=> // x Wx ox; apply: wlog_neg => q'p. suffices Vx: x \in V by rewrite (pgroupP pV) // -ox order_dvdG. have [sWH nWH] := andP nsWH; rewrite (subsetP scVHV) // inE (subsetP sWH) //=. have coVx: coprime #|V| #[x] by rewrite ox (pnat_coprime pV) // pnatE. rewrite -cycle_subG (coprime_cent_Phi pV coVx) //. have: V :&: W \subset 'Phi(V); last apply: subset_trans. rewrite -quotient_sub1; last by rewrite subIset ?(subset_trans sWH) ?orbT. by rewrite quotientIG ?tiWb. rewrite commg_subI //; first by rewrite subsetI subxx (subset_trans sVH). by rewrite cycle_subG inE Wx (subsetP nVH) // (subsetP sWH). have{scVHV} scVH: 'C_H(V) = V by apply/eqP; rewrite eqEsubset scVHV subsetI sVH. without loss{IHquo} indecomposableV: / forall U W, U \x W = V -> G \subset 'N(U) :&: 'N(W) -> U = 1 \/ U = V. - pose decV UW := let: (U, W) := UW in [&& U \x W == V, G \subset 'N(U) :&: 'N(W), U != 1 & W != 1]. case: (pickP decV) => [[A B /=] | indecV]; last first. apply=> U W defUW nUW_G; have:= indecV (U, W); rewrite /= -defUW nUW_G eqxx. by rewrite -negb_or; case/pred2P=> ->; [left | right; rewrite dprodg1]. rewrite subsetI -!andbA => /and5P[/eqP/dprodP[[U W -> ->{A B}]]]. move=> defUW _ tiUW nUG nWG ntU ntW _. have [sUH sWH]: U \subset H /\ W \subset H. by apply/andP; rewrite -mulG_subG defUW. have [nsUH nsWH]: U <| H /\ W <| H. by rewrite /normal !(subset_trans sHG) ?andbT. by rewrite -(quo2_plength1 _ nsUH nsWH) ?tiUW ?IHquo. have nsFb: 'F(H / V) <| G / V by rewrite gFnormal_trans ?quotient_normal. have{nsVG nsFb} [/= U defU sVU nsUG] := inv_quotientN nsVG nsFb. have{nsUG} [sUG nUG] := andP nsUG. have [solU nVU] := (solvableS sUG solG, subset_trans sUG nVG). have sUH: U \subset H by rewrite -(quotientSGK nVU sVH) -defU Fitting_sub. have [K hallK nKR]: exists2 K : {group gT}, p^'.-Hall(U) K & R \subset 'N(K). by apply: coprime_Hall_exists; rewrite ?(coprimeSg sUH) ?(subset_trans sRG). have [sKU p'K _] := and3P hallK; have{sUG} sKG := subset_trans sKU sUG. have coVK: coprime #|V| #|K| := pnat_coprime pV p'K. have [sKH nVK] := (subset_trans sKU sUH, subset_trans sKU nVU). have{defV} p'Ub: p^'.-group (U / V). rewrite -defU -['F(H / V)](nilpotent_pcoreC p (Fitting_nil _)) /=. by rewrite p_core_Fitting -defV trivg_pcore_quotient dprod1g pcore_pgroup. have{p'Ub} sylV: p.-Sylow(U) V by rewrite /pHall sVU pV -card_quotient. have{sKU} mulVK: V * K = U. apply/eqP; rewrite eqEcard mul_subG //= coprime_cardMg //. by rewrite (card_Hall sylV) (card_Hall hallK) partnC. have [sKN sNH]: K \subset 'N_H(K) /\ 'N_H(K) \subset H. by rewrite subsetIl subsetI sKH normG. have [solN nVN] := (solvableS sNH solH, subset_trans sNH nVH). have{solU hallK sUH nUG} defH: V * 'N_H(K) = H. have nsUH: U <| H by apply/andP; rewrite (subset_trans sHG). by rewrite -(mulSGid sKN) mulgA mulVK (Hall_Frattini_arg solU nsUH hallK). have [P sylP nPR]: exists2 P : {group _}, p.-Sylow('N_H(K)) P & R \subset 'N(P). apply: coprime_Hall_exists (coprimeSg sNH coHR) solN. by rewrite normsI ?norms_norm. have [sPN pP _]: [/\ P \subset 'N_H(K), p.-group P & _] := and3P sylP. have [sPH nKP]: P \subset H /\ P \subset 'N(K) by apply/andP; rewrite -subsetI. have nVP := subset_trans sPH nVH. have coKP: coprime #|K| #|P| by rewrite coprime_sym (pnat_coprime pP). have{sylP} sylVP: p.-Sylow(H) (V <*> P). rewrite pHallE /= norm_joinEr ?mul_subG //= -defH -!LagrangeMl. rewrite partnM // part_pnat_id // -!card_quotient //. by apply/eqP; congr (_ * _)%N; apply: card_Hall; apply: quotient_pHall. have [trKP | {sylV sVU nVU}ntKP] := eqVneq [~: K, P] 1. suffices sylVH: p.-Sylow(H) V. rewrite p_elt_gen_length1 // (_ : p_elt_gen p H = V). rewrite /pHall pcore_sub pcore_pgroup /= pnatNK. by apply: pnat_dvd pV; apply: dvdn_indexg. rewrite -(genGid V) -(setIidPr sVH); congr <<_>>; apply/setP=> x. rewrite !inE; apply: andb_id2l => Hx. by rewrite (mem_normal_Hall sylVH) /normal ?sVH. suffices sPV: P \subset V by rewrite -(joing_idPl sPV). suffices sPU: P \subset U by rewrite (sub_normal_Hall sylV) //; apply/andP. have cUPb: P / V \subset 'C_(H / V)(U / V). rewrite subsetI morphimS // -mulVK quotientMidl quotient_cents2r //. by rewrite commGC trKP sub1G. rewrite -(quotientSGK nVP sVU) (subset_trans cUPb) //. by rewrite -defU cent_sub_Fitting ?quotient_sol. have{sylVP} dxV: [~: V, K] \x 'C_V(K) = V by apply: coprime_abelian_cent_dprod. have tiVsub_VcK: 'C_V(K) = 1 \/ 'C_V(K) = V. apply: (indecomposableV _ [~: V, K]); first by rewrite dprodC. rewrite -mulHR -defH -mulgA mul_subG // subsetI. by rewrite commg_norml cents_norm // centsC subIset // -abelianE cVV. have nK_NR: 'N_H(K) * R \subset 'N(K) by rewrite mul_subG ?subsetIr. have nV_NR: 'N_H(K) * R \subset 'N(V) by rewrite mul_subG. by rewrite normsR // normsI ?norms_cent. have{tiVsub_VcK dxV} [defVK tiVcK]: [~: V, K] = V /\ 'C_V(K) = 1. have [tiVcK | eqC] := tiVsub_VcK; first by rewrite -{2}dxV // tiVcK dprodg1. rewrite (card1_trivg (pnat_1 (pgroupS _ pV) p'K)) ?comm1G ?eqxx // in ntKP. by rewrite -scVH subsetI sKH centsC -eqC subsetIr. have eqVncK: 'N_V(K) = 'C_V(K) := coprime_norm_cent nVK (pnat_coprime pV p'K). have{eqVncK} tiVN: V :&: 'N_H(K) = 1 by rewrite setIA (setIidPl sVH) eqVncK. have{sPN} tiVP: V :&: P = 1 by apply/trivgP; rewrite -tiVN setIS. have{U defU mulVK} defK: 'F('N_H(K)) = K. have [injV imV] := isomP (quotient_isom nVN tiVN). rewrite -(im_invm injV) -injm_Fitting ?injm_invm //= {2}imV /=. rewrite -quotientMidl defH defU -mulVK quotientMidl morphim_invmE. by rewrite morphpre_restrm quotientK // -group_modr // setIC tiVN mul1g. have scKH: 'C_H(K) \subset K. rewrite -{2}defK; apply: subset_trans (cent_sub_Fitting _) => //. by rewrite defK subsetI subsetIr setIS // cent_sub. have{nVN} ntKR0: [~: K, R0] != 1. rewrite (sameP eqP commG1P); apply: contra ntKP => cR0K. have ZgrK: Zgroup K by apply: ZgroupS ZgrCHR0; rewrite subsetI sKH. have{ZgrK} cycK: cyclic K by rewrite nil_Zgroup_cyclic // -defK Fitting_nil. have{cycK} sNR_K: [~: 'N_H(K), R] \subset K. apply: subset_trans scKH; rewrite subsetI; apply/andP; split. by rewrite (subset_trans (commSg R sNH)) // commGC commg_subr. suffices: 'N(K)^`(1) \subset 'C(K). by apply: subset_trans; rewrite commgSS ?subsetIr. rewrite der1_min ?cent_norm //= -ker_conj_aut (isog_abelian (first_isog _)). exact: abelianS (Aut_conj_aut K 'N(K)) (Aut_cyclic_abelian cycK). suffices sPV: P \subset V by rewrite -(setIidPr sPV) tiVP commG1. have pPV: p.-group (P / V) := quotient_pgroup V pP. rewrite -quotient_sub1 // subG1 (card1_trivg (pnat_1 pPV _)) //. apply: pgroupS (quotient_pgroup V p'K). apply: subset_trans (quotientS V sNR_K). by rewrite quotientR // -quotientMidl defH -quotientR ?defHR ?quotientS. have nKR0: R0 \subset 'N(K) := subset_trans sR0R nKR. have mulKR0: K * R0 = K <*> R0 by rewrite norm_joinEr. have sKR0_G : K <*> R0 \subset G by rewrite -mulKR0 -mulHR mulgSS. have nV_KR0: K <*> R0 \subset 'N(V) := subset_trans sKR0_G nVG. have solKR0: solvable (K <*> R0) by apply: solvableS solG. have coKR0: coprime #|K| #|R0| by rewrite (coprimeSg sKH) ?(coprimegS sR0R). have r'K: r^'.-group K. by rewrite /pgroup p'natE -?prime_coprime // coprime_sym -oR0. have tiKcV: 'C_K(V) = 1. by apply/trivgP; rewrite -tiVN -{2}scVH -setIIr setICA setIC setSI. have tiKR0cV: 'C_(K <*> R0)(V) = 1. set C := 'C_(K <*> R0)(V); apply/eqP; apply: contraR ntKR0 => ntC. have nC_KR0: K <*> R0 \subset 'N(C) by rewrite normsI ?normG ?norms_cent. rewrite -subG1 -(coprime_TIg coKR0) commg_subI ?subsetI ?subxx //=. suff defC: C == R0 by rewrite -(eqP defC) (subset_trans (joing_subl K R0)). have sC_R0: C \subset R0. rewrite -[C](coprime_mulG_setI_norm mulKR0) ?norms_cent //= tiKcV mul1g. apply: subsetIl. rewrite eqEsubset sC_R0; apply: contraR ntC => not_sR0C. by rewrite -(setIidPr sC_R0) prime_TIg ?oR0. have{nKR0 mulKR0 sKR0_G solKR0 nV_KR0} oCVR0: #|'C_V(R0)| = p. case: (eqVneq 'C_V(R0) 1) => [tiVcR0 | ntCVR0]. case/negP: ntKR0; rewrite -subG1/= commGC -tiKcV. have defKR0: K ><| R0 = K <*> R0 by rewrite sdprodE ?coprime_TIg. have odd_KR0: odd #|K <*> R0| := oddSg sKR0_G oddG. apply: odd_prime_sdprod_abelem_cent1 abelV nV_KR0 _ _; rewrite // ?oR0 //=. by rewrite -mulKR0 pgroupM p'K /pgroup oR0 pnatE. have [x defC]: exists x, 'C_V(R0) = <[x]>. have ZgrC: Zgroup 'C_V(R0) by apply: ZgroupS ZgrCHR0; apply: setSI. apply/cyclicP; apply: (forall_inP ZgrC); apply/SylowP; exists p => //. by rewrite /pHall subxx indexgg (pgroupS (subsetIl V _)). rewrite defC; apply: nt_prime_order => //; last by rewrite -cycle_eq1 -defC. by rewrite (exponentP eV) // -cycle_subG -defC subsetIl. have tiPcR0: 'C_P(R0) = 1. rewrite -(setIidPl (joing_subl P V)) setIIl TI_Ohm1 //=. set C := 'C_(P <*> V)(R0); suffices <-: 'C_V(R0) = 'Ohm_1(C). by rewrite setIC -setIIl tiVP (setIidPl (sub1G _)). have pPV: p.-group (P <*> V) by rewrite norm_joinEl // pgroupM pP. have pC: p.-group C := pgroupS (subsetIl _ _) pPV. have abelCVR0: p.-abelem 'C_V(R0) by rewrite prime_abelem ?oCVR0. have sCV_C: 'C_V(R0) \subset C by rewrite setSI ?joing_subr. apply/eqP; rewrite eqEcard -(Ohm1_id abelCVR0) OhmS //=. have [-> | ntC] := eqVneq C 1; first by rewrite subset_leq_card ?OhmS ?sub1G. rewrite (Ohm1_id abelCVR0) oCVR0 (Ohm1_cyclic_pgroup_prime _ pC) //=. have ZgrC: Zgroup C by rewrite (ZgroupS _ ZgrCHR0) ?setSI // join_subG sPH. apply: (forall_inP ZgrC); apply/SylowP; exists p => //. by apply/pHallP; rewrite part_pnat_id. have defP: [~: P, R0] = P. have solvP := pgroup_sol pP; have nPR0 := subset_trans sR0R nPR. have coPR0: coprime #|P| #|R0| by rewrite (coprimeSg sPH) ?(coprimegS sR0R). by rewrite -{2}(coprime_cent_prod nPR0) // tiPcR0 mulg1. have{nVH} IHsub: forall X : {group gT}, P <*> R0 \subset 'N(X) -> X \subset K -> (#|V <*> X <*> P| < #|H|) || (#|R0| < #|R|) -> [~: X, P] = 1. - move=> X; rewrite join_subG; case/andP=> nXP nXR0 sXK. set H0 := V <*> X <*> P => ltG0G; have sXH := subset_trans sXK sKH. have sXH0: X \subset H0 by rewrite /H0 joingC joingA joing_subr. have sH0H: H0 \subset H by rewrite !join_subG sVH sXH. have nH0R0: R0 \subset 'N(H0). by rewrite 2?normsY ?nXR0 ?(subset_trans sR0R) // (subset_trans sRG). have Op'H0: 'O_p^'(H0) = 1. have [sOp' nOp'] := andP (pcore_normal _ _ : 'O_p^'(H0) <| H0). have p'Op': p^'.-group 'O_p^'(H0) by apply: pcore_pgroup. apply: card1_trivg (pnat_1 (pgroupS _ pV) p'Op'). rewrite -scVH subsetI (subset_trans sOp') //= centsC; apply/setIidPl. rewrite -coprime_norm_cent ?(pnat_coprime pV p'Op') //. by rewrite (setIidPl (subset_trans _ nOp')) // /H0 -joingA joing_subl. exact: subset_trans (subset_trans sH0H nVH). have Op'HR0: 'O_p^'([~: H0, R0]) = 1. apply/trivgP; rewrite -Op'H0 pcore_max ?pcore_pgroup // gFnormal_trans //. by rewrite /(_ <| _) commg_norml andbT commg_subl. have{ltG0G IHsub} p1_HR0: p.-length_1 [~: H0, R0]. by apply: IHsub ltG0G => //=; rewrite mul_subG ?normG. have{p1_HR0} sPOpHR0: P \subset 'O_p([~: H0, R0]). rewrite sub_Hall_pcore //; last by rewrite -defP commSg ?joing_subr. rewrite /pHall pcore_sub pcore_pgroup /= -(pseries_pop2 _ Op'HR0). rewrite -card_quotient ?normal_norm ?pseries_normal // -/(pgroup _ _). by rewrite -{1}((_ :=P: _) p1_HR0) (quotient_pseries [::_; _]) pcore_pgroup. apply/trivgP; have <-: K :&: 'O_p([~: H0, R0]) = 1. by rewrite setIC coprime_TIg // (pnat_coprime (pcore_pgroup p _)). by rewrite commg_subI // subsetI ?sPOpHR0 ?sXK //= gFnorm_trans // normsRl. have{defH sR0R} [defH defR0]: V * K * P = H /\ R0 :=: R. suffices: (V * K * P == H) && (R0 :==: R) by do 2!case: eqP => // ->. apply: contraR ntKP; rewrite -subG1 !eqEcard sR0R ?mul_subG //= negb_and. rewrite -!ltnNge -!norm_joinEr // 1?normsY //; move/IHsub=> -> //. by rewrite join_subG nKP (subset_trans sR0R). move: IHsub defP oR0 rR0 ZgrCHR0 coKR0 ntKR0 tiKR0cV oCVR0 tiPcR0. rewrite {R0}defR0 ltnn => IHsub defP oR rR ZgrCHR coKR ntKR tiKRcV oCVR tiPcR. have mulVK: V * K = V <*> K by rewrite norm_joinEr. have oVK: #|V <*> K| = (#|V| * #|K|)%N by rewrite -mulVK coprime_cardMg. have tiVK_P: V <*> K :&: P = 1. have sylV: p.-Sylow(V <*> K) V. by rewrite /pHall pV -divgS joing_subl //= oVK mulKn. apply/trivgP; rewrite -tiVP subsetI subsetIr. rewrite (sub_normal_Hall sylV) ?subsetIl ?(pgroupS (subsetIr _ P)) //=. by rewrite /normal joing_subl join_subG normG. have{mulVK oVK} oH: (#|H| = #|V| * #|K| * #|P|)%N. by rewrite -defH mulVK -oVK (TI_cardMg tiVK_P). have{oH tiVK_P} IHsub: forall X : {group gT}, P <*> R \subset 'N(X) -> X \subset K -> X :=: K \/ X \subset 'C(P). - move=> X nX_PR sXK; have p'X: p^'.-group X := pgroupS sXK p'K. have nXP: P \subset 'N(X) := subset_trans (joing_subl P R) nX_PR. apply/predU1P; rewrite eqEcard sXK; case: leqP => //= ltXK. apply/commG1P; rewrite {}IHsub // orbF (norm_joinEr (normsY _ _)) //=. rewrite TI_cardMg /=; last first. by apply/trivgP; rewrite -tiVK_P setSI ?genS ?setUS. rewrite oH ltn_pmul2r ?cardG_gt0 // norm_joinEr ?(subset_trans sXK) //. by rewrite coprime_cardMg ?ltn_pmul2l ?(pnat_coprime pV). have defKP: [~: K, P] = K. have sKP_K: [~: K, P] \subset K by rewrite commg_subl. have{sKP_K} [|//|cP_KP] := IHsub _ _ sKP_K. by rewrite join_subG /= commg_normr normsR. by case/eqP: ntKP; rewrite -coprime_commGid ?(commG1P cP_KP) ?(solvableS sKH). have nKPR: P <*> R \subset 'N(K) by rewrite join_subG nKP. have coPR: coprime #|P| #|R| by rewrite (coprimeSg sPH). have{scKH} tiPRcK: 'C_(P <*> R)(K) = 1. have tiPK: P :&: K = 1 by rewrite setIC coprime_TIg. have tiPcK: 'C_P(K) = 1. by apply/trivgP; rewrite /= -{1}(setIidPl sPH) -setIA -tiPK setIS. have tiRcK: 'C_R(K) = 1. by rewrite prime_TIg ?oR // centsC (sameP commG1P eqP). have mulPR: P * R = P <*> R by rewrite norm_joinEr. by rewrite -(coprime_mulG_setI_norm mulPR) ?tiPcK ?mul1g ?norms_cent. have [K1 | ntK]:= eqsVneq K 1; first by rewrite K1 comm1G eqxx in ntKR. have [K1 | [q q_pr q_dv_K]] := trivgVpdiv K; first by case/eqP: ntK. have q_gt1 := prime_gt1 q_pr. have p'q: q != p by apply: (pgroupP p'K). have{r'K} q'r: r != q by rewrite eq_sym; apply: (pgroupP r'K). have{defK} qK: q.-group K. have{defK} nilK: nilpotent K by rewrite -defK Fitting_nil. have{nilK} [_ defK _ _] := dprodP (nilpotent_pcoreC q nilK). have{IHsub} IHpi: forall pi, 'O_pi(K) = K \/ 'O_pi(K) \subset 'C(P). move=> pi; apply: IHsub (pcore_sub _ _). by rewrite gFnorm_trans // join_subG nKP. case: (IHpi q) => [<-| cPKq]; first exact: pcore_pgroup. case/eqP: ntKP; apply/commG1P; rewrite -{}defK mul_subG //. case: (IHpi q^') => // defK; case/idPn: q_dv_K. by rewrite -p'natE // -defK; apply: pcore_pgroup. pose K' := K^`(1); have charK': K' \char K := der_char 1 K. have nsK'K: K' <| K := der_normal 1 K; have [sK'K nK'K] := andP nsK'K. have nK'PR: P <*> R \subset 'N(K') := char_norm_trans charK' nKPR. have iK'K: 'C_(P <*> R / K')(K / K') = 1 -> #|K / K'| > q ^ 2. have qKb: q.-group (K / K') by apply: morphim_pgroup qK. rewrite ltnNge => trCK'; apply: contra ntKP => Kq_le_q2. suffices sPR_K': [~: P, R] \subset K'. rewrite -defP -(setIidPl sPR_K') coprime_TIg ?commG1 //. by rewrite (pnat_coprime (pgroupS _ pP) (pgroupS sK'K p'K)) ?commg_subl. rewrite -quotient_cents2 ?(char_norm_trans charK') //. suffices cPRbPrb: abelian (P <*> R / K'). by rewrite (sub_abelian_cent2 cPRbPrb) ?quotientS ?joing_subl ?joing_subr. have nKbPR: P <*> R / K' \subset 'N(K / K') by apply: quotient_norms. case cycK: (cyclic (K / K')). rewrite (isog_abelian (quotient1_isog _)) -trCK' -ker_conj_aut. rewrite (isog_abelian (first_isog_loc _ _)) //. by rewrite (abelianS (Aut_conj_aut _ _)) ?Aut_cyclic_abelian. have{cycK} [oKb abelKb]: #|K / K'| = (q ^ 2)%N /\ q.-abelem (K / K'). have sKb1: 'Ohm_1(K / K') \subset K / K' by apply: Ohm_sub. have cKbKb: abelian (K / K') by rewrite sub_der1_abelian. have: #|'Ohm_1(K / K')| >= q ^ 2. rewrite (card_pgroup (pgroupS sKb1 qKb)) leq_exp2l // ltnNge. by rewrite -p_rank_abelian -?rank_pgroup // -abelian_rank1_cyclic ?cycK. rewrite (geq_leqif (leqif_trans (subset_leqif_card sKb1) (leqif_eq _))) //. by case/andP=> sKbKb1; move/eqP->; rewrite (abelemS sKbKb1) ?Ohm1_abelem. have ntKb: K / K' != 1 by rewrite -cardG_gt1 oKb (ltn_exp2l 0). pose rPR := abelem_repr abelKb ntKb nKbPR. have: mx_faithful rPR by rewrite abelem_mx_faithful. move: rPR; rewrite (dim_abelemE abelKb ntKb) oKb pfactorK // => rPR ffPR. apply: charf'_GL2_abelian ffPR _. by rewrite quotient_odd ?(oddSg _ oddG) // join_subG (subset_trans sPH). rewrite (eq_pgroup _ (eq_negn (charf_eq (char_Fp q_pr)))). rewrite quotient_pgroup //= norm_joinEr // pgroupM. by rewrite /pgroup (pi_pnat rR) // (pi_pnat pP) // !inE eq_sym. case cKK: (abelian K); last first. have [|[dPhiK dK'] dCKP] := abelian_charsimple_special qK coKP defKP. apply/bigcupsP=> L /andP[charL]; have sLK := char_sub charL. by case/IHsub: sLK cKK => // [|-> -> //]; apply: char_norm_trans charL _. have eK: exponent K %| q. have oddK: odd #|K| := oddSg sKG oddG. have [Q [charQ _ _ eQ qCKQ]] := critical_odd qK oddK ntK; rewrite -eQ. have sQK: Q \subset K := char_sub charQ. have [<- // | cQP] := IHsub Q (char_norm_trans charQ nKPR) sQK. case/negP: ntKP; rewrite (sameP eqP commG1P) centsC. rewrite -ker_conj_aut -sub_morphim_pre // subG1 trivg_card1. rewrite (pnat_1 (morphim_pgroup _ pP) (pi_pnat (pgroupS _ qCKQ) _)) //. apply/subsetP=> a; case/morphimP=> x nKx Px ->{a}. rewrite /= astab_ract inE /= Aut_aut; apply/astabP=> y Qy. rewrite [_ y _]norm_conj_autE ?(subsetP sQK) //. by rewrite /conjg (centsP cQP y) ?mulKg. have tiPRcKb: 'C_(P <*> R / K')(K / K') = 1. rewrite -quotient_astabQ -quotientIG /=; last first. by rewrite sub_astabQ normG trivg_quotient sub1G. apply/trivgP; rewrite -quotient1 quotientS // -tiPRcK subsetI subsetIl /=. rewrite (coprime_cent_Phi qK) ?(coprimegS (subsetIl _ _)) //=. by rewrite norm_joinEr // coprime_cardMg // coprimeMr coKP. rewrite dPhiK -dK' -/K' (subset_trans (commgS _ (subsetIr _ _))) //. by rewrite astabQ -quotient_cents2 ?subsetIl // cosetpreK centsC /=. have [nK'P nK'R] := (char_norm_trans charK' nKP, char_norm_trans charK' nKR). have solK: solvable K := pgroup_sol qK. have dCKRb: 'C_K(R) / K' = 'C_(K / K')(R / K'). by rewrite coprime_quotient_cent. have abelKb: q.-abelem (K / K') by rewrite [K']dK' -dPhiK Phi_quotient_abelem. have [qKb cKbKb _] := and3P abelKb. have [tiKcRb | ntCKRb]:= eqVneq 'C_(K / K')(R / K') 1. have coK'P: coprime #|K'| #|P| by rewrite (coprimeSg sK'K). suffices sPK': P \subset K'. by case/negP: ntKP; rewrite -(setIidPr sPK') coprime_TIg ?commG1. rewrite -quotient_sub1 // -defP commGC quotientR //= -/K'. have <-: 'C_(P / K')(K / K') = 1. by apply/trivgP; rewrite -tiPRcKb setSI ?morphimS ?joing_subl. have q'P: q^'.-group P by rewrite /pgroup (pi_pnat pP) // !inE eq_sym. move: tiKcRb; have: q^'.-group (P <*> R / K'). rewrite quotient_pgroup //= norm_joinEr //. by rewrite pgroupM q'P /pgroup oR pnatE. have sPRG: P <*> R \subset G by rewrite join_subG sRG (subset_trans sPH). have coPRb: coprime #|P / K'| #|R / K'| by rewrite coprime_morph. apply: odd_prime_sdprod_abelem_cent1 abelKb _; rewrite ?quotient_norms //. - by rewrite quotient_sol // (solvableS sPRG). - by rewrite quotient_odd // (oddSg sPRG). - by rewrite /= quotientY // sdprodEY ?quotient_norms ?coprime_TIg. rewrite -(card_isog (quotient_isog nK'R _)) ?oR //. by rewrite coprime_TIg // (coprimeSg sK'K). have{ntCKRb} not_sCKR_K': ~~ ('C_K(R) \subset K'). by rewrite -quotient_sub1 ?subIset ?nK'K // dCKRb subG1. have oCKR: #|'C_K(R)| = q. have [x defCKR]: exists x, 'C_K(R) = <[x]>. have ZgrCKR: Zgroup 'C_K(R) := ZgroupS (setSI _ sKH) ZgrCHR. have qCKR: q.-group 'C_K(R) by rewrite (pgroupS (subsetIl K _)). by apply/cyclicP; apply: nil_Zgroup_cyclic (pgroup_nil qCKR). have Kx: x \in K by rewrite -cycle_subG -defCKR subsetIl. rewrite defCKR cycle_subG in not_sCKR_K' *. exact: nt_prime_order (exponentP eK x Kx) (group1_contra not_sCKR_K'). have tiCKR_K': 'C_K(R) :&: K' = 1 by rewrite prime_TIg ?oCKR. have sKR_K: [~: K, R] \subset K by rewrite commg_subl nKR. have ziKRcR: 'C_K(R) :&: [~: K, R] \subset K'. rewrite -quotient_sub1 ?subIset ?nK'K // setIC. rewrite (subset_trans (quotientI _ _ _)) // dCKRb setIA. rewrite (setIidPl (quotientS _ sKR_K)) // ?quotientR //= -/K'. by rewrite coprime_abel_cent_TI ?quotient_norms ?coprime_morph. have not_sK_KR: ~~ (K \subset [~: K, R]). by apply: contra not_sCKR_K' => sK_KR; rewrite -{1}(setIidPl sK_KR) setIAC. have tiKRcR: 'C_[~: K, R](R) = 1. rewrite -(setIidPr sKR_K) setIAC -(setIidPl ziKRcR) setIAC tiCKR_K'. by rewrite (setIidPl (sub1G _)). have cKR_KR: abelian [~: K, R]. have: 'C_[~: K, R](V) \subset [1]. rewrite -tiVN -{2}scVH -setIIr setICA setIC setIS //. exact: subset_trans sKR_K sKN. rewrite /abelian (sameP commG1P trivgP) /= -derg1; apply: subset_trans. have nKR_R: R \subset 'N([~: K, R]) by rewrite commg_normr. have sKRR_G: [~: K, R] <*> R \subset G by rewrite join_subG comm_subG. move: oCVR; have: p^'.-group ([~: K, R] <*> R). by rewrite norm_joinEr // pgroupM (pgroupS sKR_K p'K) /pgroup oR pnatE. have solKR_R := solvableS sKRR_G solG. apply: Frobenius_prime_cent_prime; rewrite ?oR ?(subset_trans _ nVG) //. by rewrite sdprodEY // coprime_TIg // (coprimeSg sKR_K). case nKR_P: (P \subset 'N([~: K, R])). have{nKR_P} nKR_PR: P <*> R \subset 'N([~: K, R]). by rewrite join_subG nKR_P commg_normr. have{nKR_PR} [dKR | cP_KR] := IHsub _ nKR_PR sKR_K. by rewrite dKR subxx in not_sK_KR. have{cP_KR} cKRb: R / K' \subset 'C(K / K'). by rewrite quotient_cents2r //= dK' -dCKP commGC subsetI sKR_K. case/negP: ntKR; rewrite (sameP eqP commG1P) centsC. by rewrite (coprime_cent_Phi qK) // dPhiK -dK' commGC -quotient_cents2. have{nKR_P} [x Px not_nKRx] := subsetPn (negbT nKR_P). have iKR: #|K : [~: K, R]| = q. rewrite -divgS // -{1}(coprime_cent_prod nKR) // TI_cardMg ?mulKn //. by rewrite setIA (setIidPl sKR_K). have sKRx_K: [~: K, R] :^ x \subset K by rewrite -{2}(normsP nKP x Px) conjSg. have nKR_K: K \subset 'N([~: K, R]) by apply: commg_norml. have mulKR_Krx: [~: K, R] * [~: K, R] :^ x = K. have maxKR: maximal [~: K, R] K by rewrite p_index_maximal ?iKR. apply: mulg_normal_maximal; rewrite ?(p_maximal_normal qK) //. by rewrite inE in not_nKRx. have ziKR_KRx: [~: K, R] :&: [~: K, R] :^ x \subset K'. rewrite /K' dK' subsetI subIset ?sKR_K // -{3}mulKR_Krx centM centJ. by rewrite setISS ?conjSg. suffices: q ^ 2 >= #|K / K'| by rewrite leqNgt iK'K. rewrite -divg_normal // leq_divLR ?cardSg //. rewrite -(@leq_pmul2l (#|[~: K, R]| ^ 2)) ?expn_gt0 ?cardG_gt0 // mulnA. rewrite -expnMn -iKR Lagrange // -mulnn -{2}(cardJg _ x) mul_cardG. by rewrite mulKR_Krx mulnAC leq_pmul2l ?muln_gt0 ?cardG_gt0 ?subset_leq_card. have tiKcP: 'C_K(P) = 1 by rewrite -defKP coprime_abel_cent_TI. have{IHsub} abelK: q.-abelem K. have [/abelem_Ohm1P->//|cPK1] := IHsub _ (gFnorm_trans _ nKPR) (Ohm_sub 1 K). rewrite -(setIid K) TI_Ohm1 ?eqxx // in ntK. by apply/eqP; rewrite -subG1 -tiKcP setIS. have{K' iK'K charK' nsK'K sK'K nK'K nK'PR} oKq2: q ^ 2 < #|K|. have K'1: K' :=: 1 by apply/commG1P. rewrite -indexg1 -K'1 -card_quotient ?normal_norm // iK'K // K'1. by rewrite -injm_subcent ?coset1_injm ?norms1 //= tiPRcK morphim1. pose S := [set Vi : {group gT} | 'C_V('C_K(Vi)) == Vi & maximal 'C_K(Vi) K]. have defSV Vi: Vi \in S -> 'C_V('C_K(Vi)) = Vi by rewrite inE; case: eqP. have maxSK Vi: Vi \in S -> maximal 'C_K(Vi) K by case/setIdP. have sSV Vi: Vi \in S -> Vi \subset V by move/defSV <-; rewrite subsetIl. have ntSV Vi: Vi \in S -> Vi :!=: 1. move=> Si; apply: contraTneq (maxgroupp (maxSK _ Si)) => ->. by rewrite /= cent1T setIT proper_irrefl. have nSK Vi: Vi \in S -> K \subset 'N(Vi). by move/defSV <-; rewrite normsI ?norms_cent // sub_abelian_norm ?subsetIl. have defV: <<\bigcup_(Vi in S) Vi>> = V. apply/eqP; rewrite eqEsubset gen_subG. apply/andP; split; first by apply/bigcupsP; apply: sSV. rewrite -(coprime_abelian_gen_cent cKK nVK) ?(pnat_coprime pV) // gen_subG. apply/bigcupsP=> Kj /= /and3P[cycKbj sKjK nKjK]. have [xb defKbj] := cyclicP cycKbj. have Kxb: xb \in K / Kj by rewrite defKbj cycle_id. set Vj := 'C_V(Kj); have [-> | ntVj] := eqsVneq Vj 1; first exact: sub1G. have nt_xb: xb != 1. apply: contra ntVj; rewrite -cycle_eq1 -defKbj -!subG1 -tiVcK. by rewrite quotient_sub1 // => sKKj; rewrite setIS ?centS. have maxKj: maximal Kj K. rewrite p_index_maximal // -card_quotient // defKbj -orderE. by rewrite (abelem_order_p (quotient_abelem Kj abelK) Kxb nt_xb). suffices defKj: 'C_K(Vj) = Kj. by rewrite sub_gen // (bigcup_max 'C_V(Kj))%G // inE defKj eqxx. have{maxKj} [_ maxKj] := maxgroupP maxKj. rewrite ['C_K(Vj)]maxKj //; last by rewrite subsetI sKjK centsC subsetIr. rewrite properEneq subsetIl andbT (sameP eqP setIidPl) centsC. by apply: contra ntVj; rewrite -subG1 -tiVcK subsetI subsetIl. pose dxp := [fun D : {set {group gT}} => \big[dprod/1]_(Vi in D) Vi]. have{} defV: \big[dprod/1]_(Vi in S) Vi = V. have [D maxD]: {D | maxset [pred E | group_set (dxp E) & E \subset S] D}. by apply: ex_maxset; exists set0; rewrite /= sub0set big_set0 groupP. have [gW sDS] := andP (maxsetp maxD); have{maxD} [_ maxD] := maxsetP maxD. have{gW} [W /= defW]: {W : {group gT} | dxp D = W} by exists (Group gW). have [eqDS | ltDS] := eqVproper sDS. by rewrite eqDS in defW; rewrite defW -(bigdprodWY defW). have{ltDS} [_ [Vi Si notDi]] := properP ltDS. have sWV: W \subset V. rewrite -(bigdprodWY defW) gen_subG. by apply/bigcupsP=> Vj Dj; rewrite sSV ?(subsetP sDS). suffices{maxD sWV defV} tiWcKi: 'C_W('C_K(Vi)) = 1. have:= notDi; rewrite -(maxD (Vi |: D)) ?setU11 ?subsetUr //= subUset sDS. rewrite sub1set Si big_setU1 //= defW dprodEY ?groupP //. by rewrite (sub_abelian_cent2 cVV) // sSV. by rewrite -(defSV Vi Si) setIAC (setIidPr sWV). apply/trivgP/subsetP=> w /setIP[Ww cKi_w]. have [v [Vv def_w v_uniq]] := mem_bigdprod defW Ww. rewrite def_w big1 ?inE // => Vj Dj; have Sj := subsetP sDS Vj Dj. have cKi_vj: v Vj \in 'C('C_K(Vi)). apply/centP=> x Ki_x; apply/commgP/conjg_fixP. apply: (v_uniq (fun Vk => v Vk ^ x)) => // [Vk Dk|]. have [[Kx _] Sk]:= (setIP Ki_x, subsetP sDS Vk Dk). by rewrite memJ_norm ?Vv // (subsetP (nSK Vk Sk)). rewrite -(mulKg x w) -(centP cKi_w) // -conjgE def_w. by apply: (big_morph (conjg^~ x)) => [y z|]; rewrite ?conj1g ?conjMg. suffices mulKji: 'C_K(Vj) * 'C_K(Vi) = K. by apply/set1gP; rewrite -tiVcK -mulKji centM setIA defSV // inE Vv. have maxKj := maxSK Vj Sj; have [_ maxKi] := maxgroupP (maxSK Vi Si). rewrite (mulg_normal_maximal _ maxKj) -?sub_abelian_normal ?subsetIl //. have [eqVji|] := eqVneq Vj Vi; first by rewrite -eqVji Dj in notDi. apply: contra => /= sKiKj; rewrite -val_eqE /= -(defSV Vj Sj). by rewrite (maxKi _ (maxgroupp maxKj) sKiKj) defSV. have nVPR: P <*> R \subset 'N(V) by rewrite join_subG nVP. have actsPR: [acts P <*> R, on S | 'JG]. apply/subsetP=> x PRx; rewrite !inE; apply/subsetP=> Vi. rewrite !inE /= => Si; rewrite -(normsP nKPR x PRx) !centJ -!conjIg centJ . by rewrite -(normsP nVPR x PRx) -conjIg (inj_eq (@conjsg_inj _ _)) maximalJ. have transPR: [transitive P <*> R, on S | 'JG]. pose ndxp D (U A B : {group gT}) := dxp (S :&: D) = U -> A * B \subset 'N(U). have nV_VK D U: ndxp D U V K. move/bigdprodWY <-; rewrite norms_gen ?norms_bigcup //. apply/bigcapsP=> Vi /setIP[Si _]. by rewrite mulG_subG nSK // sub_abelian_norm // sSV. have nV_PR D U: [acts P <*> R, on S :&: D | 'JG] -> ndxp D U P R. move=> actsU /bigdprodWY<-; rewrite -norm_joinEr ?norms_gen //. apply/subsetP=> x PRx; rewrite inE sub_conjg; apply/bigcupsP=> Vi Di. by rewrite -sub_conjg (bigcup_max (Vi :^ x)%G) //= (acts_act actsU). have [S0 | [V1 S1]] := set_0Vmem S. by case/eqP: ntV; rewrite -defV S0 big_set0. apply/imsetP; exists V1 => //; set D := orbit _ _ _. rewrite (big_setID D) /= setDE in defV. have [[U W defU defW] _ _ tiUW] := dprodP defV. rewrite defU defW in defV tiUW. have [|U1|eqUV]:= indecomposableV _ _ defV. - rewrite -mulHR -defH -mulgA mul_subG //. by rewrite subsetI (nV_VK _ _ defU) (nV_VK _ _ defW). rewrite subsetI (nV_PR _ _ _ defU) ?actsI ?acts_orbit ?subsetT //=. by rewrite (nV_PR _ _ _ defW) // actsI ?astabsC ?acts_orbit ?subsetT /=. - case/negP: (ntSV V1 S1); rewrite -subG1 -U1 -(bigdprodWY defU) sub_gen //. by rewrite (bigcup_max V1) // inE S1 orbit_refl. apply/eqP; rewrite eqEsubset (acts_sub_orbit _ actsPR) S1 andbT. apply/subsetP=> Vi Si; apply: contraR (ntSV Vi Si) => D'i; rewrite -subG1. rewrite -tiUW eqUV subsetI sSV // -(bigdprodWY defW). by rewrite (bigD1 Vi) ?joing_subl // inE Si inE. have [cSR | not_cSR] := boolP (R \subset 'C(S | 'JG)). have{cSR} sRnSV: R \subset \bigcap_(Vi in S) 'N(Vi). apply/bigcapsP=> Vi Si. by rewrite -astab1JG (subset_trans cSR) ?astabS ?sub1set. have sPRnSV: P <*> R \subset 'N(\bigcap_(Vi in S) 'N(Vi)). apply/subsetP=> x PRx; rewrite inE; apply/bigcapsP=> Vi Si. by rewrite sub_conjg -normJ bigcap_inf ?(acts_act actsPR) ?groupV. have [V1 S1] := imsetP transPR. have: P <*> R \subset 'N(V1). rewrite join_subG (subset_trans sRnSV) /= ?bigcap_inf // andbT -defP. apply: (subset_trans (commgS P sRnSV)). have:= subset_trans (joing_subl P R) sPRnSV; rewrite -commg_subr /=. by move/subset_trans; apply; apply: bigcap_inf. rewrite -afixJG; move/orbit1P => -> allV1. have defV1: V1 = V by apply: group_inj; rewrite /= -defV allV1 big_set1. case/idPn: oKq2; rewrite -(Lagrange (subsetIl K 'C(V1))). rewrite (p_maximal_index qK (maxSK V1 S1)) defV1 /= tiKcV cards1 mul1n. by rewrite (ltn_exp2l 2 1). have actsR: [acts R, on S | 'JG] := subset_trans (joing_subr P R) actsPR. have ntSRcR Vi: Vi \in S -> ~~ (R \subset 'N(Vi)) -> #|Vi| = p /\ 'C_V(R) \subset <<class_support Vi R>>. - move=> Si not_nViR; have [sVi nV] := (subsetP (sSV Vi Si), subsetP nVR). pose f v := fmval (\sum_(x in R) fmod cVV v ^@ x). have fM: {in Vi &, {morph f: u v / u * v}}. move=> u v /sVi Vu /sVi Vv; rewrite -fmvalA -big_split. by congr (fmval _); apply: eq_bigr => x Rx; rewrite /= -actAr fmodM. have injf: 'injm (Morphism fM). apply/subsetP=> v /morphpreP[Vi_v]; have Vv := sVi v Vi_v. rewrite (bigD1 Vi) //= in defV; have [[_ W _ dW] _ _ _] := dprodP defV. have [u [w [_ _ uw Uuw]]] := mem_dprod defV (group1 V). case: (Uuw 1 1) => // [||u1 w1]; rewrite ?dW ?mulg1 // !inE eq_sym /f /=. move/eqP; rewrite (big_setD1 1) // actr1 ?fmodK // fmvalA //= fmval_sum. do [case/Uuw; rewrite ?dW ?fmodK -?u1 ?group_prod //] => [x R'x | ->] //. rewrite (nt_gen_prime _ R'x) ?cycle_subG ?oR // inE in not_nViR nVR actsR. rewrite fmvalJ ?fmodK // -(bigdprodWY dW) ?mem_gen //; apply/bigcupP. exists (Vi :^ x)%G; rewrite ?memJ_conjg // (astabs_act _ actsR) Si. by apply: contraNneq not_nViR => /congr_group->. have im_f: Morphism fM @* Vi \subset 'C_V(R). apply/subsetP=> _ /morphimP[v _ Vi_v ->]; rewrite inE fmodP. apply/centP=> x Rx; red; rewrite conjgC -fmvalJ ?nV //; congr (x * fmval _). rewrite {2}(reindex_acts 'R _ Rx) ?astabsR //= actr_sum. by apply: eq_bigr => y Ry; rewrite actrM ?nV. have defCVR: Morphism fM @* Vi = 'C_V(R). apply/eqP; rewrite eqEcard im_f (prime_nt_dvdP _ _ (cardSg im_f)) ?oCVR //=. by rewrite -trivg_card1 morphim_injm_eq1 ?ntSV. rewrite -oCVR -defCVR; split; first by rewrite card_injm. apply/subsetP=> _ /morphimP[v _ Vi_v ->] /=; rewrite /f fmval_sum. have Vv := sVi v Vi_v; apply: group_prod => x Rx. by rewrite fmvalJ ?fmodK ?nV // mem_gen // imset2_f. have{not_cSR} [V1 S1 not_nV1R]: exists2 V1, V1 \in S & ~~ (R \subset 'N(V1)). by move: not_cSR; rewrite astabC; case/subsetPn=> v; rewrite afixJG; exists v. set D := orbit 'JG%act R V1. have oD: #|D| = r by rewrite card_orbit astab1JG prime_TIg ?indexg1 ?oR. have oSV Vi: Vi \in S -> #|Vi| = p. move=> Si; have [z _ ->]:= atransP2 transPR S1 Si. by rewrite cardJg; case/ntSRcR: not_nV1R. have cSnS' Vi: Vi \in S -> 'N(Vi)^`(1) \subset 'C(Vi). move=> Si; rewrite der1_min ?cent_norm //= -ker_conj_aut. rewrite (isog_abelian (first_isog _)) (abelianS (Aut_conj_aut _ _)) //. by rewrite Aut_cyclic_abelian // prime_cyclic // oSV. have nVjR Vj: Vj \in S :\: D -> 'C_K(Vj) = [~: K, R]. case/setDP=> Sj notDj; set Kj := 'C_K(Vj). have [nVjR|] := boolP (R \subset 'N(Vj)). have{nVjR} sKRVj: [~: K, R] \subset Kj. rewrite subsetI {1}commGC commg_subr nKR. by rewrite (subset_trans _ (cSnS' Vj Sj)) // commgSS ?nSK. have iKj: #|K : Kj| = q by rewrite (p_maximal_index qK (maxSK Vj Sj)). have dxKR: [~: K, R] \x 'C_K(R) = K by rewrite coprime_abelian_cent_dprod. have{dxKR} [_ defKR _ tiKRcR] := dprodP dxKR. have Z_CK: Zgroup 'C_K(R) by apply: ZgroupS ZgrCHR; apply: setSI. have abelCKR: q.-abelem 'C_K(R) := abelemS (subsetIl _ _) abelK. have [qCKR _] := andP abelCKR. apply/eqP; rewrite eq_sym eqEcard sKRVj -(leq_pmul2r (ltnW q_gt1)). rewrite -{1}iKj Lagrange ?subsetIl // -{1}defKR (TI_cardMg tiKRcR). rewrite leq_pmul2l ?cardG_gt0 //= (card_pgroup qCKR). rewrite (leq_exp2l _ 1) // -abelem_cyclic // (forall_inP Z_CK) //. by rewrite (@p_Sylow _ q) // /pHall subxx indexgg qCKR. case/ntSRcR=> // _ sCVj; case/ntSRcR: not_nV1R => // _ sCV1. suffices trCVR: 'C_V(R) = 1 by rewrite -oCVR trCVR cards1 in p_pr. apply/trivgP; rewrite (big_setID D) in defV. have{defV} [[W U /= defW defU] _ _ <-] := dprodP defV. rewrite defW defU subsetI (subset_trans sCV1) /=; last first. rewrite class_supportEr -(bigdprodWY defW) genS //. apply/bigcupsP=> x Rx; rewrite (bigcup_max (V1 :^ x)%G) // inE. by rewrite (actsP actsR) //= S1 imset_f. rewrite (subset_trans sCVj) // class_supportEr -(bigdprodWY defU) genS //. apply/bigcupsP=> x Rx; rewrite (bigcup_max (Vj :^ x)%G) // inE. by rewrite (actsP actsR) // Sj andbT (orbit_transl _ (mem_orbit 'JG Vj Rx)). have sDS: D \subset S. by rewrite acts_sub_orbit //; apply: subset_trans actsPR; apply: joing_subr. have [eqDS | ltDS] := eqVproper sDS. have [fix0 | [Vj cVjP]] := set_0Vmem 'Fix_(S | 'JG)(P). case/negP: p'r; rewrite eq_sym -dvdn_prime2 // -oD eqDS /dvdn. rewrite (pgroup_fix_mod pP (subset_trans (joing_subl P R) actsPR)). by rewrite fix0 cards0 mod0n. have{cVjP} [Sj nVjP] := setIP cVjP; rewrite afixJG in nVjP. case/negP: (ntSV Vj Sj); rewrite -subG1 -tiVcK subsetI sSV // centsC -defKP. by rewrite (subset_trans _ (cSnS' Vj Sj)) // commgSS ?nSK. have [_ [Vj Sj notDj]] := properP ltDS. have defS: S = Vj |: D. apply/eqP; rewrite eqEsubset andbC subUset sub1set Sj sDS. apply/subsetP=> Vi Si; rewrite !inE orbC /= -val_eqE /= -(defSV Vi Si). have [//|notDi] := boolP (Vi \in _); rewrite -(defSV Vj Sj) /=. by rewrite !nVjR // inE ?notDi ?notDj. suffices: odd #|S| by rewrite defS cardsU1 (negPf notDj) /= oD -oR (oddSg sRG). rewrite (dvdn_odd (atrans_dvd transPR)) // (oddSg _ oddG) //. by rewrite join_subG (subset_trans sPH). 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)