proposition: Lemma FT_Dade_support_disjoint S T : S \in 'M -> T \in 'M -> gval T \notin S :^: G -> [/\ FTsupports S T = ~~ [disjoint 'A1(S) & 'A(T)] /\ {in 'A1(S) :&: 'A(T), forall x, ~~ ('C[x] \subset S) /\ 'C[x] \subset T}, [exists x, FTsupports S (T :^ x)] = ~~ [disjoint 'A1~(S) & 'A~(T)] & [disjoint 'A1~(S) & 'A~(T)] \/ [disjoint 'A1~(T) & 'A~(S)]].
proof: Proof. move: S T; pose NC S T := gval T \notin S :^: G. have part_a2 S T (maxS : S \in 'M) (maxT : T \in 'M) (ncST : NC S T) : {in 'A1(S) :&: 'A(T), forall x, ~~ ('C[x] \subset S) /\ 'C[x] \subset T}. - move=> x /setIP[/setD1P[ntx Ss_x] ATx]. have coxTs: coprime #[x] #|T`_\s|. apply: (coprime_dvdl (order_dvdG Ss_x)). by have [_ ->] := FT_Dade_support_partition. have [z /setD1P[ntz Ts_z] /setD1P[_ /setIP[Tn_x czx]]] := bigcupP ATx. set n := FTtype T != 1%N in Tn_x. have typeT: FTtype T == n.+1. have notTs_x: x \notin T`_\s. apply: contra ntx => Ts_x. by rewrite -order_eq1 -dvdn1 -(eqnP coxTs) dvdn_gcd dvdnn order_dvdG. apply: contraLR ATx => typeT; rewrite FTsupp_eq1 // ?inE ?ntx //. move: (FTtype_range T) typeT; rewrite -mem_iota /n. by do 5!case/predU1P=> [-> // | ]. have defTs: T`_\s = T`_\F. by apply/esym/Fcore_eq_FTcore; rewrite // (eqP typeT); case n. have [U Ux defTn]: exists2 U : {group gT}, x \in U & T`_\F ><| U = T^`(n)%g. have [[U K] /= complU] := kappa_witness maxT. have defTn: T`_\s ><| U = T^`(n)%g. by rewrite def_FTcore // (sdprod_FTder maxT complU). have nsTsTn: T`_\s <| T^`(n)%g by case/sdprod_context: defTn. have [sTsTn nTsTn] := andP nsTsTn. have hallTs: \pi(T`_\s).-Hall(T^`(n)%g) T`_\s. by rewrite defTs (pHall_subl _ (der_sub n T) (Fcore_Hall T)) //= -defTs. have hallU: \pi(T`_\s)^'.-Hall(T^`(n)%g) U. by apply/sdprod_Hall_pcoreP; rewrite /= (normal_Hall_pcore hallTs). have solTn: solvable T^`(n)%g := solvableS (der_sub n T) (mmax_sol maxT). rewrite coprime_sym coprime_pi' // in coxTs. have [|y Tn_y] := Hall_subJ solTn hallU _ coxTs; rewrite cycle_subG //. exists (U :^ y)%G; rewrite // -defTs. by rewrite -(normsP nTsTn y Tn_y) -sdprodJ defTn conjGid. have uniqCx: 'M('C[x]) = [set T]. have:= FTtypeI_II_facts maxT typeT defTn; rewrite !ltnS leq_b1 -cent_set1. case=> _ -> //; first by rewrite -cards_eq0 cards1. by rewrite sub1set !inE ntx. by apply/trivgPn; exists z; rewrite //= -defTs inE Ts_z cent_set1 cent1C. split; last by case/mem_uniq_mmax: uniqCx. by apply: contra ncST => /(eq_uniq_mmax uniqCx maxS)->; apply: orbit_refl. have part_a1 S T (maxS : S \in 'M) (maxT : T \in 'M) (ncST : NC S T) : FTsupports S T = ~~ [disjoint 'A1(S) & 'A(T)]. - apply/existsP/pred0Pn=> [[x /and3P[ASx not_sCxS sCxT]] | [x /andP[A1Sx Atx]]]. have [_ [/subsetP]] := FTsupport_facts maxS; set D := finset _. have Dx: x \in D by rewrite !inE ASx. move=> /(_ x Dx) A1x /(_ x Dx)uniqCx /(_ x Dx)[_ _ /setDP[ATx _] _]. by rewrite (eq_uniq_mmax uniqCx maxT sCxT); exists x; apply/andP. exists x; rewrite (subsetP (FTsupp1_sub maxS)) //=. by apply/andP/part_a2=> //; apply/setIP. have part_b S T (maxS : S \in 'M) (maxT : T \in 'M) (ncST : NC S T) : [exists x, FTsupports S (T :^ x)] = ~~ [disjoint 'A1~(S) & 'A~(T)]. - apply/existsP/pred0Pn=> [[x] | [y /andP[/= A1GSy AGTy]]]. rewrite part_a1 ?mmaxJ // => [/pred0Pn[y /andP/=[A1Sy ATyx]]|]; last first. by rewrite /NC -(rcoset_id (in_setT x)) orbit_rcoset. rewrite FTsuppJ mem_conjg in ATyx; exists (y ^ x^-1); apply/andP; split. by apply/bigcupP; exists y => //; rewrite imset2_f ?rcoset_refl ?inE. apply/bigcupP; exists (y ^ x^-1) => //. by rewrite mem_class_support ?rcoset_refl. have{AGTy} [x2 ATx2 x2R_yG] := bigcupP AGTy. have [sCx2T | not_sCx2T] := boolP ('C[x2] \subset T); last first. have [_ _ _ [injA1G pGI pGP]] := FT_Dade_support_partition. have{pGI pGP} tiA1g: trivIset [set 'A1~(M) | M : {group gT} in 'M^G]. case: FTtypeP_pair_cases => [/forall_inP/pGI/and3P[] // | [M [L]]]. by case=> _ W W1 W2 defW1 /pGP[]/and3P[_ /(trivIsetS (subsetUr _ _))]. have [_ _ injMG sM_MG] := mmax_transversalP gT. have [_ [sDA1T _] _] := FTsupport_facts maxT. have [[z1 maxSz] [z2 maxTz]] := (sM_MG S maxS, sM_MG T maxT). case/imsetP: ncST; exists (z1 * z2^-1)%g; first by rewrite inE. rewrite conjsgM; apply/(canRL (conjsgK _))/congr_group/injA1G=> //. apply/eqP/idPn=> /(trivIsetP tiA1g)/pred0Pn[]; try exact: imset_f. exists y; rewrite !FT_Dade1_supportJ /= A1GSy andbT. by apply/bigcupP; exists x2; rewrite // (subsetP sDA1T) ?inE ?ATx2. have{x2R_yG} /imsetP[z _ def_y]: y \in x2 ^: G. by rewrite /'R_T {}sCx2T mul1g class_support_set1l in x2R_yG. have{A1GSy} [x1 A1Sx1] := bigcupP A1GSy; rewrite {y}def_y -mem_conjgV. rewrite class_supportGidr ?inE {z}//. case/imset2P=> _ z /rcosetP[y Hy ->] _ def_x2. exists z^-1%g; rewrite part_a1 ?mmaxJ //; last first. by rewrite /NC (orbit_transl _ (mem_orbit _ _ _)) ?inE. apply/pred0Pn; exists x1; rewrite /= A1Sx1 FTsuppJ mem_conjgV; apply/bigcupP. pose ddS := FT_Dade1_hyp maxS; have [/andP[sA1S _] _ notA1_1 _ _] := ddS. have [ntx1 Sx1] := (memPn notA1_1 _ A1Sx1, subsetP sA1S _ A1Sx1). have [coHS defCx1] := (Dade_coprime ddS A1Sx1 A1Sx1, Dade_sdprod ddS A1Sx1). rewrite def_FTsignalizer1 // in coHS defCx1. have[u Ts_u /setD1P[_ cT'ux2]] := bigcupP ATx2. exists u => {Ts_u}//; rewrite 2!inE -(conj1g z) (can_eq (conjgK z)) ntx1. suffices{u cT'ux2} ->: x1 = (y * x1).`_(\pi('R_S x1)^'). by rewrite -consttJ -def_x2 groupX. have /setIP[_ /cent1P cx1y]: y \in 'C_G[x1]. by case/sdprod_context: defCx1 => /andP[/subsetP->]. rewrite consttM // (constt1P _) ?p_eltNK ?(mem_p_elt (pgroup_pi _)) // mul1g. have piR'_Cx1: \pi('R_S x1)^'.-group 'C_S[x1] by rewrite coprime_pi' in coHS. by rewrite constt_p_elt ?(mem_p_elt piR'_Cx1) // inE Sx1 cent1id. move=> S T maxS maxT ncST; split; first split; auto. apply/orP/idPn; rewrite negb_or -part_b // => /andP[suppST /negP[]]. without loss{suppST} suppST: T maxT ncST / FTsupports S T. move=> IH; case/existsP: suppST => x /IH {IH}. rewrite FT_Dade1_supportJ (orbit_transl _ (mem_orbit _ _ _)) ?in_setT //. by rewrite mmaxJ => ->. have{suppST} [y /and3P[ASy not_sCyS sCyT]] := existsP suppST. have Dy: y \in [set z in 'A0(S) | ~~ ('C[z] \subset S)] by rewrite !inE ASy. have [_ [_ /(_ y Dy) uCy] /(_ y Dy)[_ coTcS _ typeT]] := FTsupport_facts maxS. rewrite -mem_iota -(eq_uniq_mmax uCy maxT sCyT) !inE in coTcS typeT. apply/negbNE; rewrite -part_b /NC 1?orbit_sym // negb_exists. apply/forallP=> x; rewrite part_a1 ?mmaxJ ?negbK //; last first. by rewrite /NC (orbit_transl _ (mem_orbit _ _ _)) ?in_setT // orbit_sym. rewrite -setI_eq0 -subset0 FTsuppJ -bigcupJ big_distrr; apply/bigcupsP=> z Sxz. rewrite conjD1g /= -setDIl coprime_TIg ?setDv //= cardJg. rewrite -(Fcore_eq_FTcore maxT _) ?inE ?orbA; last by have [->] := typeT. by rewrite (coprimegS _ (coTcS z _)) ?(subsetP (FTsupp1_sub0 _)) ?setSI ?gFsub. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice) mathcomp(fintype tuple finfun bigop prime ssralg poly finset center) mathcomp(fingroup morphism perm automorphism quotient action finalg zmodp) mathcomp(gfunctor gproduct cyclic commutator nilpotent pgroup) mathcomp(sylow hall abelian maximal frobenius) mathcomp(matrix mxalgebra mxrepresentation vector) odd_order(BGsection1 BGsection3 BGsection7 BGsection10) odd_order(BGsection14 BGsection15 BGsection16) mathcomp(algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4 PFsection5)