proposition: Lemma kappa_structure M U K (Ms := M`_\sigma) : M \in 'M -> kappa_complement M U K -> [/\ [/\ (Ms ><| U) ><| K = M, cyclic K & abelian (M^`(1) / Ms)], K :!=: 1 -> Ms ><| U = M^`(1) /\ abelian U, forall X, X \subset U -> X :!=: 1 -> 'C_Ms(X) != 1 -> [/\ 'M('C(X)) = [set M], cyclic X & \tau2(M).-group X], abelian <<\bigcup_(x in Ms^#) 'C_U[x]>> & U :!=: 1 -> exists U0, [/\ gval U0 \subset U, exponent (gval U0) = exponent U & [Frobenius Ms <*> U0 = Ms ><| U0]]].
proof: Proof. move=> maxM complU; have [hallU hallK _] := complU. have [hallE defM _ regUK cUU] := kappa_compl_context maxM complU. have [[_ E _ defE]] := sdprodP defM. have [nsUE sKE mulUK nUK tiUK] := sdprod_context defE. rewrite defE -{1 2}mulUK mulgA => defMl /mulGsubP[nMsU nMsK] tiMsE. have [/andP[sMsM nMsM] [sUE nUE]] := (pcore_normal _ M : Ms <| M, andP nsUE). rewrite norm_joinEr // mulUK in hallE. have [[sEM s'M_E _] [sUM sk'U _]] := (and3P hallE, and3P hallU). have defMsU: Ms ><| U = Ms <*> U. by apply: sdprodEY nMsU (trivgP _); rewrite -tiMsE -mulUK setIS ?mulG_subl. have{} defM: Ms <*> U ><| K = M. rewrite sdprodE ?normsY ?coprime_TIg //=; first by rewrite norm_joinEr. rewrite -(sdprod_card defMsU) coprimeMl andbC regular_norm_coprime //=. by rewrite (coprimegS sKE) ?(pnat_coprime (pcore_pgroup _ _)). rewrite defMsU quotient_der //= -/Ms -{2}defMl -mulgA mulUK. rewrite quotientMidl -quotient_der ?(subset_trans sEM) //. rewrite quotient_abelian ?(der_mmax_compl_abelian maxM hallE) //. set part_c := forall U, _; have c_holds: part_c. move=> X sXU ntX nregMsX; have sXE := subset_trans sXU sUE. have [x /setIP[Ms_x cXx] ntx] := trivgPn _ nregMsX. have Ms1x: x \in Ms^# by apply/setD1P. have piCx_hyp: {in X^#, forall x', x' \in ('C_M[x])^# /\ \sigma(M)^'.-elt x'}. move=> x' /setD1P[ntx' Xx']; have Ex' := subsetP sXE x' Xx'. rewrite 3!inE ntx' (subsetP sEM) ?(mem_p_elt s'M_E) //=. by rewrite (subsetP _ _ Xx') ?sub_cent1. have piCx x' X1x' := let: conj c e := piCx_hyp x' X1x' in pi_of_cent_sigma maxM Ms1x c e. have t2X: \tau2(M).-group X. apply/pgroupP=> p p_pr /Cauchy[] // x' Xx' ox'. have X1x': x' \in X^# by rewrite !inE Xx' -order_gt1 ox' prime_gt1. have [[]|[]] := piCx _ X1x'; last by rewrite /p_elt ox' pnatE. case/idPn; have:= mem_p_elt (pgroupS sXU sk'U) Xx'. by rewrite /p_elt ox' !pnatE // => /norP[]. suffices cycX: cyclic X. split=> //; have [x' defX] := cyclicP cycX. have X1x': x' \in X^# by rewrite !inE -cycle_eq1 -cycle_subG -defX ntX /=. have [[kX _]|[_ _]] := piCx _ X1x'; last by rewrite defX cent_cycle. rewrite -(setIid X) coprime_TIg ?eqxx // {2}defX in ntX. rewrite (pnat_coprime t2X (sub_pgroup _ kX)) // => p kp. by rewrite inE /= negb_and rank_kappa ?orbT. have [E2 hallE2 sXE2] := Hall_superset (sigma_compl_sol hallE) sXE t2X. rewrite abelian_rank1_cyclic; last first. exact: abelianS sXE2 (tau2_compl_abelian maxM hallE hallE2). have [p _ ->] := rank_witness X; rewrite leqNgt; apply: contra nregMsX => rpX. have t2p: p \in \tau2(M) by rewrite (pnatPpi t2X) // -p_rank_gt0 ltnW. rewrite -(setIidPr (subset_trans sXE sEM)) in rpX. case/p_rank_geP: rpX => A; rewrite pnElemI -setIdE; case/setIdP=> Ep2A sAX. rewrite -subG1; have [_ _ <- _ _] := tau2_context maxM t2p Ep2A. by rewrite setIS ?centS. have hallU_E: Hall E U := pHall_Hall (pHall_subl sUE sEM hallU). have UtypeF := FTtypeF_complement maxM hallE hallU_E nsUE. set k'U13 := ({in _, _}) in UtypeF. have/UtypeF{k'U13}UtypeF: k'U13. move=> x /setD1P[]; rewrite -order_gt1 -pi_pdiv. set p := pdiv _ => pi_x_p Ux t13x. apply: contraNeq (pnatPpi (mem_p_elt sk'U Ux) pi_x_p) => nreg_x. apply/orP; right; rewrite unlock /= inE /= (pnatPpi t13x) //=. have sxM: <[x]> \subset M by rewrite cycle_subG (subsetP sUM). move: pi_x_p; rewrite -p_rank_gt0 /= -(setIidPr sxM) => /p_rank_geP[P]. rewrite pnElemI -setIdE => /setIdP[EpP sPx]; apply/exists_inP; exists P => //. by rewrite (subG1_contra _ nreg_x) //= -cent_cycle setIS ?centS. have [K1 | ntK] := altP (K :=P: 1). rewrite {2}K1 cyclic1; rewrite K1 mulg1 in mulUK; rewrite -mulUK in hallE. have ltM'M := sol_der1_proper (mmax_sol maxM) (subxx _) (mmax_neq1 maxM). suffices /UtypeF[[A0 [_ abA0 genA0]] frobM]: U :!=: 1. by split => //; apply: abelianS abA0; rewrite gen_subG; apply/bigcupsP. apply: contraNneq (proper_subn ltM'M); rewrite -{1}defMl => ->. by rewrite K1 !mulg1 Msigma_der1. have PmaxM: M \in 'M_'P by rewrite inE maxM -(trivg_kappa maxM hallK) andbT. have [_ _ [_ _ _ [cycZ _ _ _ _] [_ _ _ defM']]] := Ptype_embedding PmaxM hallK. have{cycZ cUU} [cycK cUU] := (cyclicS (joing_subl _ _) cycZ, cUU ntK). split=> // [_||/UtypeF[] //]; first split=> //. apply/eqP; rewrite eq_sym eqEcard -(leq_pmul2r (cardG_gt0 K)). have [nsMsU_M _ mulMsU _ _] := sdprod_context defM. rewrite (sdprod_card defM) (sdprod_card defM') der1_min ?normal_norm //=. by rewrite -(isog_abelian (sdprod_isog defM)) cyclic_abelian. by apply: abelianS cUU; rewrite gen_subG -big_distrr subsetIl. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq choice div fintype) mathcomp(path bigop finset prime fingroup morphism perm automorphism) mathcomp(quotient action gproduct gfunctor pgroup cyclic commutator) mathcomp(center gseries nilpotent sylow abelian maximal hall frobenius) odd_order(BGsection1 BGsection2 BGsection3 BGsection4 BGsection5) odd_order(BGsection6 BGsection7 BGsection9 BGsection10 BGsection12) odd_order(BGsection13 BGsection14)