proposition: Theorem coprime_odd_faithful_Ohm1 gT p (A G : {group gT}) : p.-group G -> A \subset 'N(G) -> coprime #|G| #|A| -> odd #|G| -> A \subset 'C('Ohm_1(G)) -> A \subset 'C(G).
proof: Proof. move=> pG nGA coGA oddG; rewrite !(centsC A) => cAG1. have [-> | ntG] := eqsVneq G 1; first exact: sub1G. have{oddG ntG} [p_pr oddp]: prime p /\ odd p. have [p_pr p_dv_G _] := pgroup_pdiv pG ntG. by rewrite !odd_2'nat in oddG *; rewrite pnatE ?(pgroupP oddG). without loss defR: G pG nGA coGA cAG1 / [~: G, A] = G. move=> IH; have solG := pgroup_sol pG. rewrite -(coprime_cent_prod nGA) ?mul_subG ?subsetIr //=. have sRG: [~: G, A] \subset G by rewrite commg_subl. rewrite IH ?coprime_commGid ?(pgroupS sRG) ?commg_normr ?(coprimeSg sRG) //. by apply: subset_trans cAG1; apply: OhmS. have [|[defPhi defG'] defC] := abelian_charsimple_special pG coGA defR. apply/bigcupsP=> H /andP[chH abH]; have sHG := char_sub chH. have nHA := char_norm_trans chH nGA. rewrite centsC coprime_abelian_faithful_Ohm1 ?(coprimeSg sHG) //. by rewrite centsC (subset_trans (OhmS 1 sHG)). have abelZ: p.-abelem 'Z(G) by apply: center_special_abelem. have cAZ: {in 'Z(G), centralised A} by apply/centsP; rewrite -defC subsetIr. have cGZ: {in 'Z(G), centralised G} by apply/centsP; rewrite subsetIr. have defG1: 'Ohm_1(G) = 'Z(G). apply/eqP; rewrite eqEsubset -{1}defC subsetI Ohm_sub cAG1 /=. by rewrite -(Ohm1_id abelZ) OhmS ?center_sub. rewrite (subset_trans _ (subsetIr G _)) // defC -defG1 -{1}defR gen_subG /=. apply/subsetP=> _ /imset2P[x a Gx Aa ->]; rewrite commgEl. set u := x^-1; set v := x ^ a; pose w := [~ v, u]. have [Gu Gv]: u \in G /\ v \in G by rewrite groupV memJ_norm ?(subsetP nGA). have Zw: w \in 'Z(G) by rewrite -defG' mem_commg. rewrite (OhmE 1 pG) mem_gen // !inE expn1 groupM //=. rewrite expMg_Rmul /commute ?(cGZ w) // bin2odd // expgM. case/(abelemP p_pr): abelZ => _ /(_ w)-> //. rewrite expg1n mulg1 expgVn -conjXg (sameP commgP eqP) cAZ // -defPhi. by rewrite (Phi_joing pG) joingC mem_gen // inE (Mho_p_elt 1) ?(mem_p_elt pG). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div fintype) mathcomp(bigop prime binomial finset fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor commutator) mathcomp(ssralg finalg zmodp cyclic center pgroup finmodule gseries) mathcomp(nilpotent sylow abelian maximal hall extremal) mathcomp(matrix mxalgebra mxrepresentation mxabelem)