proposition: Lemma FTtype345_bridge_coherence calS1 tau1 i j X Y : coherent_with calS1 M^# tau tau1 -> (alpha_ i j)^\tau = X + Y -> cfConjC_subset calS1 calS0 -> {subset calS1 <= irr M} -> j != 0 -> Y \in 'Z[map tau1 calS1] -> '[Y, X] = 0 -> '[Y] = n ^+ 2 -> X = delta *: (eta_ i j - eta_ i 0).
proof: Proof. move=> cohS1 Dalpha sS10 irrS1 nz_j S1_Y oYX nY_n2. have [[_ Ddelta _ Nn] [[Itau1 Ztau1] _]] := (FTtype345_constants, cohS1). have [|z Zz defY] := zchar_expansion _ S1_Y. rewrite map_inj_in_uniq; first by case: sS10. by apply: sub_in2 (Zisometry_inj Itau1); apply: mem_zchar. have nX_2: '[X] = 2%:R. apply: (addrI '[Y]); rewrite -cfnormDd // addrC -Dalpha norm_alpha //. by rewrite addrC nY_n2. have Z_X: X \in 'Z[irr G]. rewrite -[X](addrK Y) -Dalpha rpredB ?Zalpha_tau // defY big_map big_seq. by apply: rpred_sum => psi S1psi; rewrite rpredZ_Cint // Ztau1 ?mem_zchar. apply: eq_signed_sub_cTIiso => // y Vy; rewrite -[X](addrK Y) -Dalpha -/delta. rewrite !cfunE !cycTIiso_restrict //; set rhs := delta * _. rewrite Dade_id ?defA0 //; last by rewrite setUC inE mem_class_support. have notM'y: y \notin M'. by have:= subsetP (prDade_supp_disjoint pddM) y Vy; rewrite inE. have Wy: y \in W :\: W2 by move: Vy; rewrite !inE => /andP[/norP[_ ->]]. rewrite !cfunE 2?{1}prTIirr_id // prTIsign0 scale1r Ddelta // cfunE -mulrBr. rewrite -/rhs (cfun_on0 (seqInd_on _ Szeta)) // mulr0 subr0. rewrite (ortho_cycTIiso_vanish ctiWG) ?subr0 // -/sigma. apply/orthoPl=> _ /mapP[_ /(cycTIirrP defW)[i1 [j1 ->]] ->]. rewrite defY cfdot_suml big_map big1_seq //= => psi S1psi. by rewrite cfdotZl (coherent_ortho_cycTIiso MtypeP sS10) ?irrS1 ?mulr0. 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)