proposition: Lemma Ohm1_stab_Ohm1_SCN_series : odd p -> p.-group G -> 'Ohm_1('C_G(Z)) \subset 'C_G(A / Z | 'Q).
proof: Proof. have [-> | ntG] := eqsVneq G 1; first by rewrite !(setIidPl (sub1G _)) Ohm1. move=> p_odd pG; have{ntG} [p_pr _ _] := pgroup_pdiv pG ntG. case/SCN_P: SCN_A => /andP[sAG nAG] _; have pA := pgroupS sAG pG. have pCGZ : p.-group 'C_G(Z) by rewrite (pgroupS _ pG) // subsetIl. rewrite {pCGZ}(OhmE 1 pCGZ) gen_subG; apply/subsetP=> x; rewrite 3!inE -andbA. rewrite -!cycle_subG => /and3P[sXG cZX xp1] /=; have cXX := cycle_abelian x. have nZX := cents_norm cZX; have{nAG} nAX := subset_trans sXG nAG. pose XA := <[x]> <*> A; pose C := 'C(<[x]> / Z | 'Q); pose CA := A :&: C. pose Y := <[x]> <*> CA; pose W := 'Ohm_1(Y). have sXC: <[x]> \subset C by rewrite sub_astabQ nZX (quotient_cents _ cXX). have defY : Y = <[x]> * CA by rewrite -norm_joinEl // normsI ?nAX ?normsG. have{nAX} defXA: XA = <[x]> * A := norm_joinEl nAX. suffices{sXC}: XA \subset Y. rewrite subsetI sXG /= sub_astabQ nZX centsC defY group_modl //= -/Z -/C. by rewrite subsetI sub_astabQ defXA quotientMl //= !mulG_subG; case/and4P. have sZCA: Z \subset CA by rewrite subsetI sZA [C]astabQ sub_cosetpre. have cZCA: CA \subset 'C(Z) by rewrite subIset 1?(sub_abelian_cent2 cAA). have sZY: Z \subset Y by rewrite (subset_trans sZCA) ?joing_subr. have{cZCA cZX} cZY: Y \subset 'C(Z) by rewrite join_subG cZX. have{cXX nZX} sY'Z : Y^`(1) \subset Z. rewrite der1_min ?cents_norm //= -/Y defY quotientMl // abelianM /= -/Z -/CA. rewrite !quotient_abelian // ?(abelianS _ cAA) ?subsetIl //=. by rewrite /= quotientGI ?Ohm_sub // quotient_astabQ subsetIr. have{sY'Z cZY} nil_classY: nil_class Y <= 2. by rewrite nil_class2 (subset_trans sY'Z ) // subsetI sZY centsC. have pY: p.-group Y by rewrite (pgroupS _ pG) // join_subG sXG subIset ?sAG. have sXW: <[x]> \subset W. by rewrite [W](OhmE 1 pY) ?genS // sub1set !inE -cycle_subG joing_subl. have{nil_classY pY sXW sZY sZCA} defW: W = <[x]> * Z. rewrite -[W](setIidPr (Ohm_sub _ _)) /= -/Y {1}defY -group_modl //= -/Y -/W. congr (_ * _); apply/eqP; rewrite eqEsubset {1}[Z](OhmE 1 pA). rewrite subsetI setIAC subIset //; first by rewrite sZCA -[Z]Ohm_id OhmS. rewrite sub_gen ?setIS //; apply/subsetP=> w Ww; rewrite inE. by apply/eqP; apply: exponentP w Ww; apply: exponent_Ohm1_class2. have{sXG sAG} sXAG: XA \subset G by rewrite join_subG sXG. have{sXAG} nilXA: nilpotent XA := nilpotentS sXAG (pgroup_nil pG). have sYXA: Y \subset XA by rewrite defY defXA mulgS ?subsetIl. rewrite -[Y](nilpotent_sub_norm nilXA) {nilXA sYXA}//= -/Y -/XA. suffices: 'N_XA('Ohm_1(Y)) \subset Y by apply/subset_trans/setIS/gFnorms. rewrite {XA}defXA -group_modl ?normsG /= -/W ?{W}defW ?mulG_subl //. rewrite {Y}defY mulgS // subsetI subsetIl {CA C}sub_astabQ subIset ?nZA //= -/Z. rewrite (subset_trans (quotient_subnorm _ _ _)) //= quotientMidr /= -/Z. rewrite -quotient_sub1 ?subIset ?cent_norm ?orbT //. rewrite (subset_trans (quotientI _ _ _)) ?coprime_TIg //. rewrite (@pnat_coprime p) // -/(p.-group _) ?quotient_pgroup {pA}//= -pgroupE. rewrite -(setIidPr (cent_sub _)) p'group_quotient_cent_prime //. by rewrite (dvdn_trans (dvdn_quotient _ _)) ?order_dvdn. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism quotient) mathcomp(action commutator gproduct gfunctor ssralg) mathcomp(countalg finalg zmodp cyclic pgroup center gseries) mathcomp(nilpotent sylow abelian finmodule)