proposition: Proposition SCN_normed_constrained p P A : p.-Sylow(G) P -> A \in 'SCN_2(P) -> normed_constrained A.
proof: Proof. move=> sylP; rewrite 2!inE -andbA => /and3P[nsAP /eqP defCA lt1mA]. have [sAP nAP]:= andP nsAP. have pP := pHall_pgroup sylP; have pA := pgroupS sAP pP. have abA: abelian A by rewrite /abelian -{1}defCA subsetIr. have prP: P \proper G := mFT_pgroup_proper pP. have ntA: A :!=: 1 by rewrite -rank_gt0 ltnW. pose pi := \pi(A); simpl in pi. have [p_pr pdvA [r oApr]] := pgroup_pdiv pA ntA. have{r oApr} def_pi: pi =i (p : nat_pred). by move=> p'; rewrite !inE oApr primesX // primes_prime ?inE. have def_pi' := eq_negn def_pi; have defK := eq_pcore _ def_pi'. pose Z := 'Ohm_1('Z(P)); have sZ_ZP: Z \subset 'Z(P) by apply: Ohm_sub. have sZP_A: 'Z(P) \subset A by rewrite -defCA setIS ?centS. have sZA := subset_trans sZ_ZP sZP_A. have nsA1: 'Ohm_1(A) <| P by apply: gFnormal_trans. pose inZor1 B := B \subset Z \/ #|Z| = p /\ Z \subset B. have [B [E2_B nsBP sBZ]]: exists B, [/\ B \in 'E_p^2(A), B <| P & inZor1 B]. have pZP: p.-group 'Z(P) by apply: pgroupS (center_sub _) pP. have pZ: p.-group Z by apply: pgroupS sZ_ZP pZP. have abelZ: p.-abelem Z by rewrite Ohm1_abelem ?center_abelian. have nsZP: Z <| P := sub_center_normal sZ_ZP; have [sZP nZP] := andP nsZP. case: (eqVneq Z 1). rewrite -(setIidPr sZ_ZP); move/TI_Ohm1; rewrite setIid. by move/(trivg_center_pgroup pP)=> P1; rewrite -subG1 -P1 sAP in ntA. case/(pgroup_pdiv pZ)=> _ _ [[|k] /=]; rewrite -/Z => oZ; last first. have: 2 <= 'r_p(Z) by rewrite p_rank_abelem // oZ pfactorK. case/p_rank_geP=> B; rewrite /= -/Z => Ep2Z_B; exists B. rewrite (subsetP (pnElemS _ _ sZA)) //. case/setIdP: Ep2Z_B; case/setIdP=> sBZ _ _; split=> //; last by left. by rewrite sub_center_normal ?(subset_trans sBZ). pose BZ := ('Ohm_1(A) / Z) :&: 'Z(P / Z). have ntBz: BZ != 1. rewrite meet_center_nil ?quotient_nil ?(pgroup_nil pP) ?quotient_normal //. rewrite -subG1 quotient_sub1 ?(subset_trans (normal_sub nsA1) nZP) //= -/Z. apply: contraL lt1mA => sA1Z; rewrite -(pfactorK 1 p_pr) -oZ -rank_Ohm1. by rewrite -(rank_abelem abelZ) -leqNgt rankS. have lt1A1: 1 < logn p #|'Ohm_1(A)| by rewrite -p_rank_abelian -?rank_pgroup. have [B [sBA1 nsBP oB]] := normal_pgroup pP nsA1 lt1A1. exists B; split=> //; last do [right; split=> //]. rewrite 2!inE (subset_trans sBA1) ?Ohm_sub // oB pfactorK //. by rewrite (abelemS sBA1) ?Ohm1_abelem. apply/idPn=> s'BZ; have: B :&: Z = 1 by rewrite setIC prime_TIg ?oZ. move/TI_Ohm1; apply/eqP; rewrite meet_center_nil ?(pgroup_nil pP) //. by rewrite -cardG_gt1 oB (ltn_exp2l 0 _ (prime_gt1 p_pr)). split; rewrite ?(sub_proper_trans sAP) // => X Y sAX prX. rewrite inE defK -andbA (eq_pgroup _ def_pi'); case/and3P=> sYX p'Y nYA. move: E2_B; rewrite 2!inE -andbA; case/and3P=> sBA abelB dimB2. have [pB cBB _] := and3P abelB. have ntB: B :!=: 1 by case: (eqsVneq B 1) dimB2 => // ->; rewrite cards1 logn1. have cBA b: b \in B -> A \subset 'C[b]. by move=> Bb; rewrite -cent_set1 centsC sub1set (subsetP abA) ?(subsetP sBA). have solCB (b : gT): b != 1 -> solvable 'C[b]. by move=> ntb; rewrite mFT_sol ?mFT_cent1_proper. wlog{sAX prX} [b B'b defX]: X Y p'Y nYA sYX / exists2 b, b \in B^# & 'C[b] = X. move=> IH; have nYB := subset_trans sBA nYA. rewrite -(coprime_abelian_gen_cent1 cBB _ nYB); last first. - by rewrite coprime_sym (pnat_coprime pB). - apply: contraL dimB2 => /cyclicP[x defB]. have Bx: x \in B by rewrite defB cycle_id. rewrite defB -orderE (abelem_order_p abelB Bx) ?(pfactorK 1) //. by rewrite -cycle_eq1 -defB. rewrite gen_subG; apply/bigcupsP=> b B'b. have [ntb Bb]:= setD1P B'b; have sYbY: 'C_Y[b] \subset Y := subsetIl _ _. have{IH} sYbKb: 'C_Y[b] \subset 'O_p^'('C[b]). rewrite IH ?(pgroupS sYbY) ?subsetIr //; last by exists b. by rewrite normsI // ?normsG ?cBA. have{sYbKb} sYbKXb: 'C_Y[b] \subset 'O_p^'('C_X(<[b]>)). apply: subset_trans (pcoreS _ (subsetIr _ _)). by rewrite /= cent_gen cent_set1 subsetI setSI. rewrite (subset_trans sYbKXb) // p'core_cent_pgroup ?mFT_sol //. rewrite /psubgroup ?(pgroupS _ pB) cycle_subG //. by rewrite (subsetP sAX) ?(subsetP sBA). wlog Zb: b X Y defX B'b p'Y nYA sYX / b \in Z. move=> IH; case Zb: (b \in Z); first exact: IH Zb. case/setD1P: B'b => ntb Bb; have solX := solCB b ntb; rewrite defX in solX. case: sBZ => [sBZ | [oZ sZB]]; first by rewrite (subsetP sBZ) in Zb. have defB: Z * <[b]> = B. apply/eqP; rewrite eqEcard mulG_subG sZB cycle_subG Bb. have obp := abelem_order_p abelB Bb ntb. rewrite (card_pgroup pB) /= (eqP dimB2) TI_cardMg -/#[_] ?oZ ?obp //. rewrite -obp in p_pr; case: (prime_subgroupVti [group of Z] p_pr) => //. by rewrite cycle_subG Zb. pose P1 := P :&: X; have sP1P: P1 \subset P := subsetIl _ _. have pP1 := pgroupS sP1P pP. have [P2 sylP2 sP12] := Sylow_superset (subsetIr _ _) pP1. have defP1: P1 = 'C_P(B). rewrite -defB centM /= -/Z setIA /cycle cent_gen cent_set1 defX. by rewrite [P :&: _](setIidPl _) // centsC (subset_trans sZ_ZP) ?subsetIr. have dimPP1: logn p #|P : P1| <= 1. by rewrite defP1 logn_quotient_cent_abelem ?normal_norm ?(eqP dimB2). have{dimPP1} nsP12: P1 <| P2. have pP2 := pHall_pgroup sylP2. have: logn p #|P2 : P1| <= 1. apply: leq_trans dimPP1; rewrite dvdn_leq_log //. rewrite -(dvdn_pmul2l (cardG_gt0 [group of P1])) !Lagrange ?subsetIl //. rewrite -(part_pnat_id pP2) (card_Hall sylP). by rewrite partn_dvd ?cardSg ?subsetT. rewrite -(pfactorK 1 p_pr) -pfactor_dvdn ?prime_gt0 // -p_part. rewrite part_pnat_id ?(pnat_dvd (dvdn_indexg _ _)) //=. case: (primeP p_pr) => _ dv_p; move/dv_p=> {dv_p}. case/pred2P=> oP21; first by rewrite -(index1g sP12 oP21) normal_refl. by rewrite (p_maximal_normal pP2) ?p_index_maximal ?oP21. have nsZP1_2: 'Z(P1) <| P2 by rewrite gFnormal_trans. have sZKp: Z \subset 'O_{p^', p}(X). suff: 'Z(P1) \subset 'O_{p^', p}(X). apply: subset_trans; rewrite subsetI {1}defP1 (subset_trans sZB). by rewrite (subset_trans sZ_ZP) ?subIset // orbC centS. by rewrite subsetI normal_sub. apply: odd_p_abelian_constrained sylP2 (center_abelian _) nsZP1_2 => //. exact: mFT_odd. have coYZ: coprime #|Y| #|Z|. by rewrite oZ coprime_sym (pnat_coprime _ p'Y) ?pnatE ?inE. have nYZ := subset_trans sZA nYA. have <-: [~: Y, Z] * 'C_Y(Z) = Y. exact: coprime_cent_prod (solvableS sYX solX). set K := 'O_p^'(X); have [nKY nKZ]: Y \subset 'N(K) /\ Z \subset 'N(K). by rewrite !gFnorm_trans ?(subset_trans sZA) ?normsG // -defX cBA. rewrite mul_subG //. have coYZK: coprime #|Y / K| #|'O_p(X / K)|. by rewrite coprime_sym coprime_morphr ?(pnat_coprime (pcore_pgroup _ _)). rewrite -quotient_sub1 ?comm_subG // -(coprime_TIg coYZK) subsetI. rewrite /= -quotient_pseries2 !quotientS ?commg_subl //. by rewrite (subset_trans (commgSS sYX sZKp)) ?commg_subr //= gFnorm. have: 'O_p^'('C_X(Z)) \subset K. rewrite p'core_cent_pgroup // /psubgroup /pgroup oZ pnat_id //. by rewrite -defX (subset_trans sZA) ?cBA. apply: subset_trans; apply: subset_trans (pcoreS _ (subsetIr _ _)). have: cyclic Z by rewrite prime_cyclic ?oZ. case/cyclicP=> z defZ; have Zz: z \in Z by rewrite defZ cycle_id. rewrite subsetI setSI //= (IH z) ?subsetIr ?(pgroupS (subsetIl _ _)) //. - by rewrite defZ /= cent_gen cent_set1. - rewrite !inE -cycle_eq1 -defZ trivg_card_le1 oZ -ltnNge prime_gt1 //=. by rewrite (subsetP sZB). by rewrite normsI // norms_cent // cents_norm // centsC (subset_trans sZA). set K := 'O_p^'(X); have nsKX: K <| X by apply: pcore_normal. case/setD1P: B'b => ntb Bb. have [sAX solX]: A \subset X /\ solvable X by rewrite -defX cBA ?solCB. have sPX: P \subset X. by rewrite -defX -cent_set1 centsC sub1set; case/setIP: (subsetP sZ_ZP b Zb). have [nKA nKY nKP]: [/\ A \subset 'N(K), Y \subset 'N(K) & P \subset 'N(K)]. by rewrite !(subset_trans _ (normal_norm nsKX)). have sylPX: p.-Sylow(X) P by apply: pHall_subl (subsetT _) sylP. have sAKb: A \subset 'O_{p^', p}(X). exact: (odd_p_abelian_constrained (mFT_odd _)) abA nsAP. have coYZK: coprime #|Y / K| #|'O_p(X / K)|. by rewrite coprime_sym coprime_morphr ?(pnat_coprime (pcore_pgroup _ _)). have cYAq: A / K \subset 'C_('O_p(X / K))(Y / K). rewrite subsetI -quotient_pseries2 quotientS //= (sameP commG1P trivgP). rewrite /= -quotientR // -(coprime_TIg coYZK) subsetI /= -quotient_pseries2. rewrite !quotientS ?commg_subr // (subset_trans (commgSS sAKb sYX)) //. by rewrite commg_subl /= gFnorm. have cYKq: Y / K \subset 'C('O_p(X / K)). apply: coprime_nil_faithful_cent_stab => /=. - by rewrite gFnorm_trans ?normsG ?quotientS. - by rewrite coprime_sym. - exact: pgroup_nil (pcore_pgroup _ _). apply: subset_trans (cYAq); rewrite -defCA -['C_P(A) / K](morphim_restrm nKP). rewrite injm_cent ?ker_restrm ?ker_coset ?morphim_restrm -?quotientE //. rewrite setIid (setIidPr sAP) setISS ?centS //. by rewrite pcore_sub_Hall ?morphim_pHall. by rewrite coprime_TIg ?(pnat_coprime _ (pcore_pgroup _ _)). rewrite -quotient_sub1 //= -/K -(coprime_TIg coYZK) subsetI subxx /=. rewrite -Fitting_eq_pcore ?trivg_pcore_quotient // in cYKq *. apply: subset_trans (cent_sub_Fitting (quotient_sol _ solX)). by rewrite subsetI quotientS. Qed.
imports: HB(structures) mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div choice fintype bigop) mathcomp(finset prime fingroup morphism automorphism action quotient) mathcomp(gfunctor cyclic pgroup center commutator gseries nilpotent) mathcomp(sylow abelian maximal hall) odd_order(BGsection1 BGsection6)