proposition: Lemma non_Frobenius_FTtype1_witness : [/\ abelian P0, 'r_p(P0) = 2%N & exists2 L, L \in 'M /\ P0 \subset L`_\s & exists2 x, x \in 'Ohm_1(P0)^# & [/\ ~~ ('C_K[x] \subset K'), 'N(<[x]>) \subset M & ~~ ('C[x] \subset L)]].
proof: Proof. have ntK: K :!=: 1%g := mmax_Fcore_neq1 maxM; have [sP0M pP0 _] := and3P sylP0. have hallK: \pi(K).-Hall(M) K := Fcore_Hall M. have K'p: p \notin \pi(K) by rewrite -p'groupEpi. have K'P0: \pi(K)^'.-group P0 by rewrite (pi_pgroup pP0). have [U hallU sP0U] := Hall_superset (mmax_sol maxM) sP0M K'P0. have sylP0_U: p.-Sylow(U) P0 := pHall_subl sP0U (pHall_sub hallU) sylP0. have{hallU} defM: K ><| U = M by apply/(sdprod_normal_p'HallP nsKM hallU). have{K'P0} coKP0: coprime #|K| #|P0| by rewrite coprime_pi'. have [/(_ _ _ sylP0_U)[abP0 rankP0] uCK _] := FTtypeI_II_facts maxM Mtype1 defM. have{rankP0} /eqP prankP0: 'r_p(P0) == 2%N. by rewrite eqn_leq -{1}rank_pgroup // rankP0 (p_rank_Sylow sylP0). have piP0p: p \in \pi(P0) by rewrite -p_rank_gt0 prankP0. have [L maxL sP0Ls]: exists2 L, L \in 'M & P0 \subset L`_\s. have [DpiG _ _ _] := FT_Dade_support_partition gT. have:= piSg (subsetT P0) piP0p; rewrite DpiG => /exists_inP[L maxL piLs_p]. have [_ /Hall_pi hallLs _] := FTcore_facts maxL. have [P sylP] := Sylow_exists p L`_\s; have [sPLs _] := andP sylP. have sylP_G: p.-Sylow(G) P := subHall_Sylow hallLs piLs_p sylP. have [y _ sP0_Py] := Sylow_subJ sylP_G (subsetT P0) pP0. by exists (L :^ y)%G; rewrite ?mmaxJ // FTcoreJ (subset_trans sP0_Py) ?conjSg. split=> //; exists L => //; set P1 := 'Ohm_1(P0). have abelP1: p.-abelem P1 := Ohm1_abelem pP0 abP0. have [pP1 abP1 _] := and3P abelP1. have sP10: P1 \subset P0 := Ohm_sub 1 P0; have sP1M := subset_trans sP10 sP0M. have nKP1: P1 \subset 'N(K) by rewrite (subset_trans sP1M) ?gFnorm. have nK'P1: P1 \subset 'N(K') by apply: gFnorm_trans. have{coKP0} coKP1: coprime #|K| #|P1| := coprimegS sP10 coKP0. have solK: solvable K := nilpotent_sol (Fcore_nil M). have isoP1: P1 \isog P1 / K'. by rewrite quotient_isog // coprime_TIg ?(coprimeSg (der_sub 1 K)). have{ntK} ntKK': (K / K' != 1)%g. by rewrite -subG1 quotient_sub1 ?gFnorm ?proper_subn ?(sol_der1_proper solK). have defKK': (<<\bigcup_(xbar in (P1 / K')^#) 'C_(K / K')[xbar]>> = K / K')%g. rewrite coprime_abelian_gen_cent1 ?coprime_morph ?quotient_norms //. by rewrite quotient_abelian. rewrite -(isog_cyclic isoP1) (abelem_cyclic abelP1). by rewrite -(p_rank_abelem abelP1) p_rank_Ohm1 prankP0. have [xb P1xb ntCKxb]: {xb | xb \in (P1 / K')^# & 'C_(K / K')[xb] != 1}%g. apply/sig2W/exists_inP; rewrite -negb_forall_in. apply: contra ntKK' => /eqfun_inP regKP1bar. by rewrite -subG1 /= -defKK' gen_subG; apply/bigcupsP=> xb /regKP1bar->. have [ntxb /morphimP[x nK'x P1x Dxb]] := setD1P P1xb. have ntx: x != 1%g by apply: contraNneq ntxb => x1; rewrite Dxb x1 morph1. have ntCKx: ~~ ('C_K[x] \subset K'). rewrite -quotient_sub1 ?subIset ?gFnorm // -cent_cycle subG1 /=. have sXP1: <[x]> \subset P1 by rewrite cycle_subG. rewrite coprime_quotient_cent ?(coprimegS sXP1) ?(subset_trans sXP1) ?gFsub//. by rewrite quotient_cycle ?(subsetP nK'P1) // -Dxb cent_cycle. have{uCK} UCx: 'M('C[x]) = [set M]. rewrite -cent_set1 uCK -?card_gt0 ?cards1 // ?sub1set ?cent_set1. by rewrite !inE ntx (subsetP sP0U) ?(subsetP sP10). by apply: contraNneq ntCKx => ->; rewrite sub1G. exists x; [by rewrite !inE ntx | split=> //]. rewrite (sub_uniq_mmax UCx) /= -?cent_cycle ?cent_sub //. rewrite mFT_norm_proper ?cycle_eq1 //. by rewrite mFT_sol_proper abelian_sol ?cycle_abelian. apply: contraL (leqW (p_rankS p sP0Ls)) => /(eq_uniq_mmax UCx)-> //. by rewrite prankP0 FTcore_type1 //= ltnS p_rank_gt0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice) mathcomp(fintype tuple finfun bigop order prime ssralg finset center) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct cyclic commutator gseries nilpotent pgroup) mathcomp(sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxpoly mxrepresentation mxabelem vector) mathcomp(falgebra fieldext finfield) odd_order(BGsection1 BGsection2 BGsection3 BGsection4 BGsection7) odd_order(BGsection14 BGsection15 BGsection16) mathcomp(ssrnum ssrint algC cyclotomic algnum) mathcomp(classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4 PFsection5) odd_order(PFsection6 PFsection7 PFsection8 PFsection9 PFsection10) odd_order(PFsection11)