proposition: Lemma SCN_3_Uniqueness p A : A \in 'SCN_3[p] -> A \in 'U.
proof: Proof. move=> SCN3_A; apply/idPn=> uA'. have [P] := bigcupP SCN3_A; rewrite inE => sylP /setIdP[SCN_A Age3]. have [nsAP _] := setIdP SCN_A; have [sAP nAP] := andP nsAP. have cAA := SCN_abelian SCN_A. have pP := pHall_pgroup sylP; have pA := pgroupS sAP pP. have ntA: A :!=: 1 by rewrite -rank_gt0 -(subnKC Age3). have [p_pr _ [e oA]] := pgroup_pdiv pA ntA. have{e oA} def_piA: \pi(A) =i (p : nat_pred). by rewrite /= oA pi_of_exp //; apply: pi_of_prime. have FmCAp_le2 M: M \in 'M('C(A)) -> 'r_p('F(M)) <= 2. case/setIdP=> maxM cCAM; rewrite leqNgt; apply: contra uA' => Fge3. exact: (any_rank3_Fitting_Uniqueness maxM Fge3). have sNP_mCA M: M \in 'M('C(A)) -> 'N(P) \subset M. move=> mCA_M; have Fple2 := FmCAp_le2 M mCA_M. case/setIdP: mCA_M => maxM sCAM; set F := 'F(M) in Fple2. have sNR_M R: A \subset R -> R \subset P :&: M -> 'N(R) \subset M. move=> sAR /subsetIP[sRP sRM]. pose q := if 'r(F) <= 2 then max_pdiv #|M| else s2val (rank_witness 'F(M)). have nMqR: R \subset 'N('O_q(M)) := subset_trans sRM (gFnorm _ _). have{nMqR} [Q maxQ sMqQ] := max_normed_exists (pcore_pgroup _ _) nMqR. have [p'q sNQ_M]: q != p /\ 'N(Q) \subset M. case/mem_max_normed: maxQ sMqQ; rewrite {}/q. case: leqP => [Fle2 | ]; last first. case: rank_witness => q /= q_pr -> Fge3 qQ _ sMqQ; split=> //. by case: eqP Fge3 => // ->; rewrite ltnNge Fple2. have Mqge3: 'r('O_q(M)) >= 3. rewrite (rank_pgroup (pcore_pgroup _ _)) /= -p_core_Fitting. by rewrite (p_rank_Sylow (nilpotent_pcore_Hall _ (Fitting_nil _))). have uMq: 'O_q(M)%G \in 'U. exact: (any_rank3_Fitting_Uniqueness _ Fge3 (pcore_pgroup _ _)). have uMqM := def_uniq_mmax uMq maxM (pcore_sub _ _). apply: sub_uniq_mmax (subset_trans sMqQ (normG _)) _ => //. apply: mFT_norm_proper (mFT_pgroup_proper qQ). by rewrite -rank_gt0 2?ltnW ?(leq_trans Mqge3) ?rankS. set q := max_pdiv _ => qQ _ sMqQ. have sylMq: q.-Sylow(M) 'O_q(M). by rewrite [pHall _ _ _]rank2_max_pcore_Sylow ?mFT_odd ?mmax_sol. have defNMq: 'N('O_q(M)) = M. rewrite (mmax_normal maxM (pcore_normal _ _)) // -rank_gt0. rewrite (rank_pgroup (pcore_pgroup _ _)) (p_rank_Sylow sylMq). by rewrite p_rank_gt0 pi_max_pdiv cardG_gt1 mmax_neq1. have sylMqG: q.-Sylow(G) 'O_q(M). by rewrite (mmax_sigma_Sylow maxM) ?defNMq. rewrite (sub_pHall sylMqG qQ) ?subsetT // defNMq; split=> //. have: 'r_p(G) > 2. by rewrite (leq_trans Age3) // (rank_pgroup pA) p_rankS ?subsetT. apply: contraTneq => <-; rewrite -(p_rank_Sylow sylMqG). rewrite -leqNgt -(rank_pgroup (pcore_pgroup _ _)) /=. by rewrite -p_core_Fitting (leq_trans _ Fle2) // rankS ?pcore_sub. have trCRq': [transitive 'O_p^'('C(R)), on |/|*(R; q) | 'JG]. have cstrA: normed_constrained A. by apply: SCN_normed_constrained sylP _; rewrite inE SCN_A ltnW. have pR: p.-group R := pgroupS sRP pP. have snAR: A <|<| R by rewrite (nilpotent_subnormal (pgroup_nil pR)). have A'q: q \notin \pi(A) by rewrite def_piA. rewrite -(eq_pgroup _ def_piA) in pR. have [|?] := normed_trans_superset cstrA A'q snAR pR. by rewrite (eq_pcore _ (eq_negn def_piA)) Thompson_transitivity. by rewrite (eq_pcore _ (eq_negn def_piA)). apply/subsetP=> x nRx; have maxQx: (Q :^ x)%G \in |/|*(R; q). by rewrite (actsP (norm_acts_max_norm _ _)). have [y cRy [defQx]] := atransP2 trCRq' maxQ maxQx. rewrite -(mulgKV y x) groupMr. by rewrite (subsetP sNQ_M) // inE conjsgM defQx conjsgK. apply: subsetP cRy; apply: gFsub_trans. exact: subset_trans (centS _) sCAM. have sNA_M: 'N(A) \subset M. by rewrite sNR_M // subsetI sAP (subset_trans cAA). by rewrite sNR_M // subsetI subxx (subset_trans nAP). pose P0 := [~: P, 'N(P)]. have ntP0: P0 != 1. apply/eqP=> /commG1P; rewrite centsC -(setIidPr (subsetT 'N(P))) /=. case/(Burnside_normal_complement sylP)/sdprodP=> _ /= defG nGp'P _. have prGp': 'O_p^'(G) \proper G. rewrite properT; apply: contra ntA; move/eqP=> defG'. rewrite -(setIidPl (subsetT A)) /= -defG'. by rewrite coprime_TIg // (pnat_coprime pA (pcore_pgroup _ _)). have ntGp': 'O_p^'(G) != 1. apply: contraTneq (mFT_pgroup_proper pP); rewrite -{2}defG => ->. by rewrite mul1g proper_irrefl. by have:= mFT_norm_proper ntGp' prGp'; rewrite properE gFnorm andbF. have sP0P: P0 \subset P by rewrite commg_subl. have pP0: p.-group P0 := pgroupS sP0P pP. have uNP0_mCA M: M \in 'M('C(A)) -> 'M('N(P0)) = [set M]. move=> mCA_M; have [maxM sCAM] := setIdP mCA_M. have sAM := subset_trans cAA sCAM. pose F := 'F(M); pose D := 'O_p^'(F). have cDP0: P0 \subset 'C(D). have sA1A := Ohm_sub 1 A. have nDA1: 'Ohm_1(A) \subset 'N(D). by rewrite !gFnorm_trans // gFsub_trans // normsG. have abelA1: p.-abelem 'Ohm_1(A) by rewrite Ohm1_abelem. have dimA1ge3: logn p #|'Ohm_1(A)| >= 3. by rewrite -(rank_abelem abelA1) rank_Ohm1. have coDA1: coprime #|D| #|'Ohm_1(A)|. rewrite coprime_sym (coprimeSg sA1A) //. exact: pnat_coprime pA (pcore_pgroup _ _). rewrite centsC -[D](coprime_abelian_gen_cent (abelianS sA1A cAA) nDA1) //=. rewrite gen_subG /= -/D; apply/bigcupsP=> B /and3P[cycqB sBA1 nBA1]. have abelB := abelemS sBA1 abelA1; have sBA := subset_trans sBA1 sA1A. have{cycqB} ncycB: ~~ cyclic B. move: cycqB; rewrite (abelem_cyclic (quotient_abelem _ abelA1)). rewrite card_quotient // -divgS // logn_div ?cardSg // leq_subLR addn1. by move/(leq_trans dimA1ge3); rewrite ltnS ltnNge -(abelem_cyclic abelB). have [x Bx sCxM']: exists2 x, x \in B^# & ~~ ('C[x] \subset M). suff: ~~ (\bigcup_(x in B^#) 'C[x] \subset M). case/subsetPn=> y /bigcupP[x Bx cxy] My'. by exists x; last by apply/subsetPn; exists y. have EpB: B \in 'E_p(M) by rewrite inE (subset_trans sBA sAM). apply: contra uA' => sCB_M. apply: uniq_mmaxS sBA (mFT_pgroup_proper pA) _. exact: noncyclic_cent1_sub_Uniqueness maxM EpB ncycB sCB_M. case/setD1P: Bx; rewrite -cycle_eq1 => ntx Bx. have{ntx} [L /setIdP[maxL /=]] := mmax_exists (mFT_cent_proper ntx). rewrite cent_cycle => sCxL. have{sCxM'} neLM : L != M by case: eqP sCxL sCxM' => // -> ->. have sNP_LM: 'N(P) \subset L :&: M. rewrite subsetI !sNP_mCA // inE maxL (subset_trans _ sCxL) // -cent_set1. by rewrite centS // sub1set (subsetP sBA). have sP0_LM': P0 \subset (L :&: M)^`(1). exact: subset_trans (commSg _ (normG _)) (dergS 1 sNP_LM). have DLle2: 'r(D :&: L) <= 2. apply: contraR neLM; rewrite -ltnNge -in_set1 => /rank_geP[E /nElemP[q]]. rewrite /= -/D => /pnElemP[/subsetIP[sED sEL] abelE dimE3]. have sEF: E \subset F := subset_trans sED (pcore_sub _ _). have Fge3: 'r_q(F) >= 3 by rewrite -dimE3 -p_rank_abelem // p_rankS. have qE := abelem_pgroup abelE. have uE: E \in 'U. apply: any_rank3_Fitting_Uniqueness Fge3 _ _ => //. by rewrite (rank_pgroup qE) p_rank_abelem ?dimE3. rewrite -(def_uniq_mmax uE maxM (subset_trans sEF (Fitting_sub _))). by rewrite inE maxL. have cDL_P0: P0 \subset 'C(D :&: L). have nsDM: D <| M by rewrite !gFnormal_trans. have{nsDM} [sDM nDM] := andP nsDM. have sDL: D :&: L \subset L :&: M by rewrite setIC setIS. have nsDL: D :&: L <| L :&: M by rewrite /normal sDL setIC normsIG. have [s ch_s last_s_DL] := chief_series_exists nsDL. have solLM := solvableS (subsetIl L M) (mmax_sol maxL). have solDL := solvableS sDL solLM. apply: (stable_series_cent (congr_group last_s_DL)) => //; first 1 last. rewrite coprime_sym (coprimegS (subsetIl _ _)) //. exact: pnat_coprime (pcore_pgroup _ _). have{last_s_DL}: last 1%G s \subset D :&: L by rewrite last_s_DL. rewrite /= -/P0; elim/last_ind: s ch_s => //= s U IHs. rewrite !rcons_path last_rcons /=; set V := last _ s. case/andP=> ch_s chUV sUDL; have [maxU _ nU_LM] := and3P chUV. have{maxU} /andP[/andP[sVU _] nV_LM] := maxgroupp maxU. have nVU := subset_trans sUDL (subset_trans sDL nV_LM). rewrite IHs ?(subset_trans sVU) // /stable_factor /normal sVU nVU !andbT. have nVP0 := subset_trans (subset_trans sP0_LM' (der_sub _ _)) nV_LM. rewrite commGC -sub_astabQR // (subset_trans sP0_LM') //. have /is_abelemP[q _ /andP[qUV _]]: is_abelem (U / V). exact: sol_chief_abelem solLM chUV. apply: rank2_der1_cent_chief qUV sUDL; rewrite ?mFT_odd //. exact: leq_trans (p_rank_le_rank _ _) DLle2. rewrite centsC (subset_trans cDL_P0) ?centS ?setIS //. by rewrite (subset_trans _ sCxL) // -cent_set1 centS ?sub1set. case: (ltnP 2 'r(F)) => [| Fle2]. have [q q_pr -> /= Fq3] := rank_witness [group of F]. have Mq3: 'r('O_q(M)) >= 3. rewrite (rank_pgroup (pcore_pgroup _ _)) /= -p_core_Fitting. by rewrite (p_rank_Sylow (nilpotent_pcore_Hall _ (Fitting_nil _))). have uMq: 'O_q(M)%G \in 'U. exact: any_rank3_Fitting_Uniqueness Fq3 (pcore_pgroup _ _) Mq3. apply: def_uniq_mmaxS (def_uniq_mmax uMq maxM (pcore_sub q _)); last first. exact: mFT_norm_proper ntP0 (mFT_pgroup_proper pP0). rewrite cents_norm // centsC (subset_trans cDP0) ?centS //=. rewrite -p_core_Fitting sub_pcore // => q1; move/eqnP=> ->{q1}. by apply/eqnP=> def_q; rewrite ltnNge def_q FmCAp_le2 in Fq3. rewrite (mmax_normal maxM) ?mmax_sup_id //. have sNP_M := sNP_mCA M mCA_M; have sPM := subset_trans (normG P) sNP_M. rewrite /normal comm_subG //= -/P0. have nFP: P \subset 'N(F) by apply: subset_trans (gFnorm _ _). have <-: F <*> P * 'N_M(P) = M. apply: Frattini_arg (pHall_subl (joing_subr _ _) (subsetT _) sylP). rewrite -(quotientGK (Fitting_normal M)) /= norm_joinEr //= -/F. rewrite -quotientK // cosetpre_normal -sub_abelian_normal ?quotientS //. by rewrite sub_der1_abelian ?rank2_der1_sub_Fitting ?mFT_odd ?mmax_sol. case/dprodP: (nilpotent_pcoreC p (Fitting_nil M)) => _ /= defF cDFp _. rewrite norm_joinEr //= -{}defF -(centC cDFp) -/D p_core_Fitting /= -/F. rewrite -!mulgA mul_subG //; first by rewrite cents_norm // centsC. rewrite mulgA [_ * P]mulSGid ?pcore_sub_Hall 1?(pHall_subl _ (subsetT _)) //. by rewrite mulSGid ?subsetI ?sPM ?normG // subIset // orbC normsRr. have [M mCA_M] := mmax_exists (mFT_cent_proper ntA). have [maxM sCAM] := setIdP mCA_M; have sAM := subset_trans cAA sCAM. have abelA1: p.-abelem 'Ohm_1(A) by rewrite Ohm1_abelem. have sA1A := Ohm_sub 1 A. have EpA1: 'Ohm_1(A)%G \in 'E_p(M) by rewrite inE (subset_trans sA1A). have ncycA1: ~~ cyclic 'Ohm_1(A). rewrite (abelem_cyclic abelA1) -(rank_abelem abelA1) rank_Ohm1. by rewrite -(subnKC Age3). have [x A1x sCxM']: exists2 x, x \in 'Ohm_1(A)^# & ~~ ('C[x] \subset M). suff: ~~ (\bigcup_(x in 'Ohm_1(A)^#) 'C[x] \subset M). case/subsetPn=> y /bigcupP[x A1 cxy] My'. by exists x; last by apply/subsetPn; exists y. apply: contra uA' => sCA1_M. apply: uniq_mmaxS sA1A (mFT_pgroup_proper pA) _. exact: noncyclic_cent1_sub_Uniqueness maxM EpA1 ncycA1 sCA1_M. case/setD1P: A1x; rewrite -cycle_eq1 => ntx A1x. have: 'C[x] \proper G by rewrite -cent_cycle mFT_cent_proper. case/mmax_exists=> L /setIdP[maxL sCxL]. have mCA_L: L \in 'M('C(A)). rewrite inE maxL (subset_trans _ sCxL) //= -cent_set1 centS // sub1set. by rewrite (subsetP sA1A). case/negP: sCxM'; have/uNP0_mCA := mCA_L. by rewrite (uNP0_mCA M) // => /set1_inj->. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div fintype path) mathcomp(finset prime fingroup action automorphism quotient cyclic) mathcomp(gproduct gfunctor pgroup center commutator gseries nilpotent) mathcomp(sylow abelian maximal hall) odd_order(BGsection1 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection8)