proposition: Lemma supp_FTtype345_bridge i j : j != 0 -> alpha_ i j \in 'CF(M, 'A0(M)).
proof: Proof. move=> nz_j; have [Dd Ddelta _ _] := FTtype345_constants. have Dmu2 := prTIirr_id pddM. have W1a0 x: x \in W1 -> alpha_ i j x = 0. move=> W1x; rewrite !cfunE; have [-> | ntx] := eqVneq x 1%g. by rewrite Dd // prTIirr0_1 mulr1 zeta1w1 divfK ?neq0CG ?subrr. have notM'x: x \notin M'. apply: contra ntx => M'x; have: x \in M' :&: W1 by apply/setIP. by rewrite coprime_TIg ?inE. have /sdprod_context[_ sW1W _ _ tiW21] := dprodWsdC defW. have abW2: abelian W2 := cyclic_abelian cycW2. have Wx: x \in W :\: W2. rewrite inE (contra _ ntx) ?(subsetP sW1W) // => W2x. by rewrite -in_set1 -set1gE -tiW21 inE W2x. rewrite !Dmu2 {Wx}// Ddelta // prTIsign0 scale1r !dprod_IirrE cfunE. rewrite -!(cfResE _ sW1W) ?cfDprodKl_abelian // subrr. have [s _ ->] := seqIndP Szeta. by rewrite (cfun_on0 (cfInd_normal _ _)) ?mulr0 ?subrr. apply/cfun_onP=> x; rewrite !inE defA notMtype1 /= => /norP[notM'x]. set pi := \pi(M'); have [Mx /= pi_x | /cfun0->//] := boolP (x \in M). have hallM': pi.-Hall(M) M' by rewrite Hall_pi -?(coprime_sdprod_Hall_l defM). have hallW1: pi^'.-Hall(M) W1 by rewrite -(compl_pHall _ hallM') sdprod_compl. have{pi_x} pi'x: pi^'.-elt x. apply: contraR notM'x => not_pi'x; rewrite !inE (mem_normal_Hall hallM') //. rewrite not_pi'x andbT negbK in pi_x. by rewrite (contraNneq _ not_pi'x) // => ->; apply: p_elt1. have [|y My] := Hall_subJ (mmax_sol maxM) hallW1 _ pi'x; rewrite cycle_subG //. by case/imsetP=> z Wz ->; rewrite cfunJ ?W1a0. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg poly 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 mxrepresentation mxabelem vector) odd_order(BGsection1 BGsection3 BGsection7 BGsection15 BGsection16) mathcomp(ssrnum algC classfun character integral_char inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4) odd_order(PFsection5 PFsection6 PFsection7 PFsection8 PFsection9)