proposition: Lemma coprime_der1_sdprod K H G : K ><| H = G -> coprime #|K| #|H| -> solvable K -> K \subset G^`(1) -> [~: K, H] = K /\ 'C_K(H) \subset K^`(1).
proof: Proof. case/sdprodP=> _ defG nKH tiKH coKH solK sKG'. set K' := K^`(1); have [sK'K nK'K] := andP (der_normal 1 K : K' <| K). have nK'H: H \subset 'N(K') := gFnorm_trans _ nKH. set R := [~: K, H]; have sRK: R \subset K by rewrite commg_subl. have [nRK nRH] := joing_subP (commg_norm K H : K <*> H \subset 'N(R)). have sKbK'H': K / R \subset (K / R)^`(1) * (H / R)^`(1). have defGb: (K / R) \* (H / R) = G / R. by rewrite -defG quotientMl ?cprodE // centsC quotient_cents2r. have [_ -> _ /=] := cprodP (der_cprod 1 defGb). by rewrite -quotient_der ?quotientS // -defG mul_subG. have tiKbHb': K / R :&: (H / R)^`(1) = 1. by rewrite coprime_TIg // (coprimegS (der_sub 1 _)) ?coprime_morph. have{sKbK'H' tiKbHb'} derKb: (K / R)^`(1) = K / R. by rewrite -{2}(setIidPr sKbK'H') -group_modl ?der_sub // setIC tiKbHb' mulg1. have{derKb} Kb1: K / R = 1. rewrite (contraNeq (sol_der1_proper _ (subxx (K / R)))) ?quotient_sol //. by rewrite derKb properxx. have{Kb1 sRK} defKH: [~: K, H] = K. by apply/eqP; rewrite eqEsubset sRK -quotient_sub1 ?Kb1 //=. split=> //; rewrite -quotient_sub1 ?subIset ?nK'K //= -/K'. have cKaKa: abelian (K / K') := der_abelian 0 K. rewrite coprime_quotient_cent ?quotient_norms ?coprime_morph //= -/K' -defKH. by rewrite quotientR // coprime_abel_cent_TI ?quotient_norms ?coprime_morph. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrfun ssrbool eqtype ssrnat seq div fintype finset) mathcomp(prime fingroup morphism automorphism quotient gproduct gfunctor) mathcomp(cyclic center commutator pgroup nilpotent sylow abelian hall) mathcomp(maximal) odd_order(BGsection1 BGappendixAB)