proposition: Lemma sol_coprime_Sylow_trans A G : solvable A -> A \subset 'N(G) -> coprime #|G| #|A| -> [transitive 'C_G(A), on [set P in 'Syl_p(G) | A \subset 'N(P)] | 'JG].
proof: Proof. move=> solA nGA coGA; pose AG := A <*> G; set FpA := finset _. have nG_AG: AG \subset 'N(G) by rewrite join_subG nGA normG. have [P sylP nPA] := sol_coprime_Sylow_exists solA nGA coGA. pose N := 'N_AG(P); have sAN: A \subset N by rewrite subsetI joing_subl. have trNPA: A :^: AG ::&: N = A :^: N. pose NG := 'N_G(P); have sNG_G : NG \subset G := subsetIl _ _. have nNGA: A \subset 'N(NG) by rewrite normsI ?norms_norm. apply/setP=> Ax; apply/setIdP/imsetP=> [[]|[x Nx ->{Ax}]]; last first. by rewrite conj_subG //; case/setIP: Nx => AGx; rewrite imset_f. have ->: N = A <*> NG by rewrite /N /AG !norm_joinEl // -group_modl. have coNG_A := coprimeSg sNG_G coGA; case/imsetP=> x AGx ->{Ax}. case/SchurZassenhaus_trans_actsol; rewrite ?cardJg // => y Ny /= ->. by exists y; rewrite // mem_gen 1?inE ?Ny ?orbT. have{trNPA}: [transitive 'N_AG(A), on FpA | 'JG]. have ->: FpA = 'Fix_('Syl_p(G) | 'JG)(A). by apply/setP=> Q; rewrite 4!inE afixJG. have SylP : P \in 'Syl_p(G) by rewrite inE. apply/(trans_subnorm_fixP _ SylP); rewrite ?astab1JG //. rewrite (atrans_supgroup _ (Syl_trans _ _)) ?joing_subr //= -/AG. by apply/actsP=> x /= AGx Q /=; rewrite !inE -{1}(normsP nG_AG x) ?pHallJ2. rewrite {1}/AG norm_joinEl // -group_modl ?normG ?coprime_norm_cent //=. rewrite -cent_joinEr ?subsetIr // => trC_FpA. have FpA_P: P \in FpA by rewrite !inE sylP. apply/(subgroup_transitiveP FpA_P _ trC_FpA); rewrite ?joing_subr //=. rewrite astab1JG cent_joinEr ?subsetIr // -group_modl // -mulgA. by congr (_ * _); rewrite mulSGid ?subsetIl. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq div choice) mathcomp(fintype finset prime fingroup morphism) mathcomp(automorphism quotient action gproduct gfunctor) mathcomp(commutator center pgroup finmodule nilpotent) mathcomp(sylow abelian maximal)