proposition: Theorem noncyclic_normed_sub_Uniqueness p M B : M \in 'M -> B \in 'E_p(M) -> ~~ cyclic B -> \bigcup_(K in |/|_G(B; p^')) K \subset M -> B \in 'U.
proof: Proof. move=> maxM /pElemP[sBM abelB] ncycB snbBp'_M; have [pB cBB _] := and3P abelB. have prM := mmax_proper maxM; have solM := mFT_sol prM. apply/uniq_mmaxP; exists M; symmetry; apply/eqP. rewrite eqEsubset sub1set inE maxM sBM; apply/subsetPn=> [[H0 MB_H0 neH0M]]. have:= erefl [arg max_(H > H0 | (H \in 'M(B)) && (H :!=: M)) #|H :&: M|`_p]. have [|H] := arg_maxnP; first by rewrite MB_H0; rewrite inE in neH0M. rewrite inE -andbA => /and3P[maxH sBH neHM] maxHM _ {H0 MB_H0 neH0M}. have sB_HM: B \subset H :&: M by rewrite subsetI sBH. have{sB_HM} [R sylR sBR] := Sylow_superset sB_HM pB. have [/subsetIP[sRH sRM] pR _] := and3P sylR. have [P sylP sRP] := Sylow_superset sRM pR; have [sPM pP _] := and3P sylP. have sHp'M: 'O_p^'(H) \subset M. apply: subset_trans snbBp'_M; rewrite (bigcup_max 'O_p^'(H)%G) // inE -andbA. by rewrite subsetT pcore_pgroup (subset_trans sBH) ?gFnorm. have{snbBp'_M} defMp': <<\bigcup_(K in |/|_G(P; p^')) K>> = 'O_p^'(M). have nMp'M: M \subset 'N('O_p^'(M)) by apply: gFnorm. have nMp'P := subset_trans sPM nMp'M. apply/eqP; rewrite eqEsubset gen_subG sub_gen ?andbT; last first. by rewrite (bigcup_max 'O_p^'(M)%G) // inE -andbA subsetT pcore_pgroup. apply/bigcupsP=> K; rewrite inE -andbA => /and3P[_ p'K nKP]. have sKM: K \subset M. apply: subset_trans snbBp'_M; rewrite (bigcup_max K) // inE -andbA subsetT. by rewrite p'K (subset_trans (subset_trans sBR sRP)). rewrite -quotient_sub1 ?(subset_trans sKM) //=; set Mp' := 'O__(M). have tiKp: 'O_p(M / Mp') :&: (K / _) = 1. exact: coprime_TIg (pnat_coprime (pcore_pgroup _ _) (quotient_pgroup _ _)). suffices sKMp: K / _ \subset 'O_p(M / Mp') by rewrite -(setIidPr sKMp) tiKp. rewrite -Fitting_eq_pcore ?trivg_pcore_quotient //. apply: subset_trans (cent_sub_Fitting (quotient_sol _ solM)). rewrite subsetI quotientS //= (Fitting_eq_pcore (trivg_pcore_quotient _ _)). rewrite (sameP commG1P trivgP) /= -/Mp' -tiKp subsetI commg_subl commg_subr. rewrite (subset_trans (quotientS _ sKM)) ?gFnorm //=. apply: subset_trans (pcore_sub_Hall (quotient_pHall nMp'P sylP)) _. by rewrite quotient_norms. have ntR: R :!=: 1 by case: eqP sBR ncycB => // -> /trivgP->; rewrite cyclic1. have{defMp'} sNPM: 'N(P) \subset M. have [Mp'1 | ntMp'] := eqVneq 'O_p^'(M) 1. have nsZLP: 'Z('L(P)) <| M. by apply: Puig_center_normal Mp'1 => //; apply: mFT_odd. rewrite -(mmax_normal maxM nsZLP) ?gFnorm_trans //. apply: contraNneq ntR => /(trivg_center_Puig_pgroup pP)-P1. by rewrite -subG1 -P1. rewrite -(mmax_normal maxM (pcore_normal _ _) ntMp') /= -defMp' norms_gen //. apply/subsetP=> x nPx; rewrite inE sub_conjg; apply/bigcupsP=> K. rewrite inE -andbA -sub_conjg => /and3P[_ p'K nKP]. rewrite (bigcup_max (K :^ x)%G) // inE -andbA subsetT pgroupJ p'K /=. by rewrite -(normP nPx) normJ conjSg. have sylPG := mmax_sigma_Sylow maxM sylP sNPM. have{sNPM} [sNRM sylRH]: 'N(R) \subset M /\ p.-Sylow(H) R. have [defR | ltRP] := eqVproper sRP. by split; rewrite defR // (pHall_subl _ (subsetT _)) // -defR. have [| D /setIdP[maxD sND]]:= @mmax_exists _ 'N(R). by rewrite mFT_norm_proper // (mFT_pgroup_proper pR). have/implyP := maxHM D; rewrite inE {}maxD /= leqNgt. rewrite (subset_trans (subset_trans sBR (normG R))) //= implybNN. have ltRN := nilpotent_proper_norm (pgroup_nil pP) ltRP. rewrite -(card_Hall sylR) (leq_trans (proper_card ltRN)) /=; last first. rewrite setIC -(part_pnat_id (pgroupS (subsetIr _ _) pP)) dvdn_leq //. by rewrite partn_dvd ?cardG_gt0 // cardSg // setISS. move/eqP=> defD; rewrite defD in sND; split; rewrite // -Sylow_subnorm. by rewrite (pHall_subl _ _ sylR) ?setIS // subsetI sRH normG. have sFH_RHp': 'F(H) \subset R * 'O_p^'(H). case/dprodP: (nilpotent_pcoreC p (Fitting_nil H)) => _ /= <- _ _. by rewrite p_core_Fitting mulgSS ?(pcore_sub_Hall sylRH) ?pcore_Fitting. have sFH_M: 'F(H) \subset M by rewrite (subset_trans sFH_RHp') ?mul_subG. case/(H :=P: M): neHM; have [le3r | ge2r] := ltnP 2 'r('F(H)). have [D uF_D] := uniq_mmaxP (Fitting_Uniqueness maxH le3r). by rewrite (eq_uniq_mmax uF_D maxM) // (eq_uniq_mmax uF_D maxH) ?Fitting_sub. have nHp'R: R \subset 'N('O_p^'(H)) by rewrite (subset_trans sRH) ?gFnorm. have nsRHp'H: R <*> 'O_p^'(H) <| H. rewrite sub_der1_normal //= ?join_subG ?sRH ?pcore_sub //. rewrite norm_joinEl // (subset_trans _ sFH_RHp') //. by rewrite rank2_der1_sub_Fitting ?mFT_odd // mFT_sol ?mmax_proper. have sylR_RHp': p.-Sylow(R <*> 'O_p^'(H)) R. by apply: (pHall_subl _ _ sylRH); rewrite ?joing_subl // normal_sub. rewrite (mmax_max maxH) // -(Frattini_arg nsRHp'H sylR_RHp') /=. by rewrite mulG_subG join_subG sRM sHp'M /= setIC subIset ?sNRM. 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)