proposition: Lemma kappa_compl_context M U K : M \in 'M -> kappa_complement M U K -> [/\ \sigma(M)^'.-Hall(M) (U <*> K), M`_\sigma ><| (U ><| K) = M, semiprime M`_\sigma K, semiregular U K & K :!=: 1 -> abelian U].
proof: Proof. move=> maxM [hallU hallK gsetUK]; set E := U <*> K. have mulUK: U * K = E by rewrite -(gen_set_id gsetUK) genM_join. have [[sKM kK _] [sUM sk'U _]] := (and3P hallK, and3P hallU). have tiUK: U :&: K = 1. by apply: coprime_TIg (p'nat_coprime (sub_pgroup _ sk'U) kK) => p; case/norP. have hallE: \sigma(M)^'.-Hall(M) E. rewrite pHallE /= -/E -mulUK mul_subG //= TI_cardMg //. rewrite -(partnC \kappa(M) (part_gt0 _ _)) (partn_part _ (@kappa_sigma' M)). apply/eqP; rewrite -partnI -(card_Hall hallK) mulnC; congr (_ * _)%N. by rewrite (card_Hall hallU); apply: eq_partn => p; apply: negb_or. have [K1 | ntK] := altP (K :=P: 1). rewrite K1 sdprodg1 -{1}(mulg1 U) -{1}K1 mulUK sdprod_sigma //. by split=> //; first apply: semiregular_prime; apply: semiregular1r. have PmaxM: M \in 'M_'P by rewrite inE maxM -(trivg_kappa maxM hallK) andbT. have [[V [complV defM] [cVV prK regK]] _ _ _ _] := Ptype_structure PmaxM hallK. have [[_ F _ defF] _ _ _] := sdprodP defM; rewrite defF in defM. have hallF: \sigma(M)^'.-Hall(M) F. exact/(sdprod_Hall_pcoreP (Msigma_Hall maxM)). have [a Ma /= defFa] := Hall_trans (mmax_sol maxM) hallE hallF. have [hallV _ _] := complV; set sk' := \sigma_kappa(M)^' in hallU hallV sk'U. have [nsVF sKF _ _ _] := sdprod_context defF. have [[[sVF _] [sFM _]] [sEM _]] := (andP nsVF, andP hallF, andP hallE). have hallV_F: sk'.-Hall(F) V := pHall_subl sVF sFM hallV. have hallU_E: sk'.-Hall(E) U := pHall_subl (joing_subl _ _) sEM hallU. have defV: 'O_sk'(F) = V := normal_Hall_pcore hallV_F nsVF. have hallEsk': sk'.-Hall(E) 'O_sk'(E). by rewrite [E]defFa pcoreJ pHallJ2 /= defV. have defU: 'O_sk'(E) = U by rewrite (eq_Hall_pcore hallEsk' hallU_E). have nUE: E \subset 'N(U) by rewrite -defU gFnorm. have hallK_E: \kappa(M).-Hall(E) K := pHall_subl (joing_subr _ _) sEM hallK. have hallK_F: \kappa(M).-Hall(F) K := pHall_subl sKF sFM hallK. have hallKa_E: \kappa(M).-Hall(E) (K :^ a) by rewrite [E]defFa pHallJ2. have [b Eb /= defKab] := Hall_trans (sigma_compl_sol hallE) hallK_E hallKa_E. have defVa: V :^ a = U by rewrite -defV -pcoreJ -defFa defU. split=> // [| x Kx | _]; last by rewrite -defVa abelianJ. by rewrite [U ><| K]sdprodEY ?sdprod_sigma //; case/joing_subP: nUE. rewrite -(conjgKV (a * b) x) -(normsP nUE b Eb) -defVa -conjsgM. rewrite -cent_cycle cycleJ centJ -conjIg cent_cycle regK ?conjs1g //. by rewrite -mem_conjg conjD1g conjsgM -defKab. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div path fintype bigop order) mathcomp(finset prime fingroup morphism perm automorphism quotient) mathcomp(action gproduct gfunctor pgroup cyclic center commutator) mathcomp(gseries nilpotent sylow abelian maximal hall frobenius) mathcomp(ssralg ssrnum ssrint rat) odd_order(BGsection1 BGsection3 BGsection4 BGsection5 BGsection6) odd_order(BGsection7 BGsection9 BGsection10 BGsection12 BGsection13)