proposition: Theorem abelian_charsimple_special : p.-group G -> coprime #|G| #|A| -> [~: G, A] = G -> \bigcup_(H : {group gT} | (H \char G) && abelian H) H \subset 'C(A) -> special G /\ 'C_G(A) = 'Z(G).
proof: Proof. move=> pG coGA defG /bigcupsP cChaA. have cZA: 'Z(G) \subset 'C_G(A). by rewrite subsetI center_sub cChaA // center_char center_abelian. have cChaG (H : {group gT}): H \char G -> abelian H -> H \subset 'Z(G). move=> chH abH; rewrite subsetI char_sub //= centsC -defG. rewrite comm_norm_cent_cent ?(char_norm chH) -?commg_subl ?defG //. by rewrite centsC cChaA ?chH. have cZ2GG: [~: 'Z_2(G), G, G] = 1. by apply/commG1P; rewrite (subset_trans (ucn_comm 1 G)) // ucn1 subsetIr. have{cZ2GG} cG'Z: 'Z_2(G) \subset 'C(G^`(1)). by rewrite centsC; apply/commG1P; rewrite three_subgroup // (commGC G). have{cG'Z} sZ2G'_Z: 'Z_2(G) :&: G^`(1) \subset 'Z(G). apply: cChaG; first by rewrite charI ?ucn_char ?der_char. by rewrite /abelian subIset // (subset_trans cG'Z) // centS ?subsetIr. have{sZ2G'_Z} sG'Z: G^`(1) \subset 'Z(G). rewrite der1_min ?gFnorm //; apply/derG1P. have /TI_center_nil: nilpotent (G / 'Z(G)) := quotient_nil _ (pgroup_nil pG). apply; first exact: gFnormal; rewrite /= setIC -ucn1 -ucn_central. rewrite -quotient_der ?gFnorm // -quotientGI ?ucn_subS ?quotientS1 //=. by rewrite ucn1. have sCG': 'C_G(A) \subset G^`(1). rewrite -quotient_sub1 //; last by rewrite subIset ?gFnorm. rewrite (subset_trans (quotient_subcent _ G A)) //= -[G in G / _]defG. have nGA: A \subset 'N(G) by rewrite -commg_subl defG. rewrite quotientR ?gFnorm_trans ?normG //. rewrite coprime_abel_cent_TI ?quotient_norms ?coprime_morph //. exact: sub_der1_abelian. have defZ: 'Z(G) = G^`(1) by apply/eqP; rewrite eqEsubset (subset_trans cZA). split; last by apply/eqP; rewrite eqEsubset cZA defZ sCG'. split=> //; apply/eqP; rewrite eqEsubset defZ (Phi_joing pG) joing_subl. have:= pG; rewrite -pnat_exponent => /p_natP[n expGpn]. rewrite join_subG subxx andbT /= -defZ -(subnn n.-1). elim: {2}n.-1 => [|m IHm]. rewrite (MhoE _ pG) gen_subG; apply/subsetP=> _ /imsetP[x Gx ->]. rewrite subn0 -subn1 -add1n -maxnE maxnC maxnE expnD. by rewrite expgM -expGpn expg_exponent ?groupX ?group1. rewrite cChaG ?Mho_char //= (MhoE _ pG) /abelian cent_gen gen_subG. apply/centsP=> _ /imsetP[x Gx ->] _ /imsetP[y Gy ->]. move: sG'Z; rewrite subsetI centsC => /andP[_ /centsP cGG']. apply/commgP; rewrite {1}expnSr expgM. rewrite commXg -?commgX; try by apply: cGG'; rewrite ?mem_commg ?groupX. apply/commgP; rewrite subsetI Mho_sub centsC in IHm. apply: (centsP IHm); first by rewrite groupX. rewrite -add1n -(addn1 m) subnDA -maxnE maxnC maxnE. rewrite -expgM -expnSr -addSn expnD expgM groupX //=. by rewrite Mho_p_elt ?(mem_p_elt pG). 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)