proposition: Lemma bridge_coherent S1 S2 (tau1 tau2 : {additive 'CF(L) -> 'CF(G)}) chi phi : cfConjC_subset S1 S -> coherent_with S1 L^# tau tau1 -> cfConjC_subset S2 S -> coherent_with S2 L^# tau tau2 -> {subset S2 <= [predC S1]} -> [/\ chi \in S1, phi \in 'Z[S2] & chi - phi \in 'CF(L, L^#)] -> tau (chi - phi) = tau1 chi - tau2 phi -> coherent (S1 ++ S2) L^# tau.
proof: Proof. move=> uccS1 cohS1 uccS2 cohS2 S1'2 [S1chi S2phi chi1_phi] tau_chi_phi. do [rewrite cfunD1E !cfunE subr_eq0 => /eqP] in chi1_phi. have [[uS1 sS1S _] [uS2 sS2S _]] := (uccS1, uccS2). have [[[Itau1 Ztau1] Dtau1] [[Itau2 Ztau2] Dtau2]] := (cohS1, cohS2). have [[N_S1 _ _] _ oS11 _ _] := subset_subcoherent uccS1. have [_ _ oS22 _ _] := subset_subcoherent uccS2. have nz_chi1: chi 1%g != 0; last move/mem_zchar in S1chi. by rewrite char1_eq0 ?N_S1 //; have [/memPn->] := andP oS11. have oS12: orthogonal S1 S2. apply/orthogonalP=> xi1 xi2 Sxi1 Sxi2; apply: orthoPr xi1 Sxi1. by rewrite subset_ortho_subcoherent ?sS2S //; apply: S1'2. set S3 := S1 ++ S2; pose Y := map tau1 S1 ++ map tau2 S2. have oS3: pairwise_orthogonal S3 by rewrite pairwise_orthogonal_cat oS11 oS22. have oY: pairwise_orthogonal Y. by rewrite pairwise_orthogonal_cat !map_pairwise_orthogonal ?coherent_ortho. have Z_Y: {subset Y <= 'Z[irr G]}. move=> psi; rewrite mem_cat. by case/orP=> /mapP[xi /mem_zchar] => [/Ztau1 | /Ztau2]-Zpsi ->. have normY: map cfnorm Y = map cfnorm (S1 ++ S2). rewrite !map_cat -!map_comp; congr (_ ++ _). by apply/eq_in_map => xi S1xi; rewrite /= Itau1 ?mem_zchar. by apply/eq_in_map => xi S2xi; rewrite /= Itau2 ?mem_zchar. have [tau3 defY ZItau3] := Zisometry_of_cfnorm oS3 oY normY Z_Y. have{defY} [defY1 defY2]: {in S1, tau3 =1 tau1} /\ {in S2, tau3 =1 tau2}. have/eqP := defY; rewrite map_cat eqseq_cat ?size_map //. by case/andP; split; apply/eq_in_map/eqP. exists tau3; split=> {ZItau3}// eta; rewrite zcharD1E. case/andP=> /(zchar_expansion (free_uniq (orthogonal_free oS3)))[b Zb {eta}->]. pose bS Si := \sum_(xi <- Si) b xi *: xi. have ZbS Si: bS Si \in 'Z[Si]. by rewrite /bS big_seq rpred_sum // => eta /mem_zchar/rpredZ_Cint->. rewrite big_cat /= -!/(bS _) cfunE addrC addr_eq0 linearD => /eqP-bS2_1. transitivity (tau1 (bS S1) + tau2 (bS S2)). by rewrite !raddf_sum; congr (_ + _); apply/eq_big_seq=> xi Si_xi /=; rewrite !raddfZ_Cint // -(defY1, defY2). have Z_S1_1 psi: psi \in 'Z[S1] -> psi 1%g \in Cint. by move/zchar_sub_irr=> Zpsi; apply/Cint_vchar1/Zpsi => ? /N_S1/char_vchar. apply/(scalerI nz_chi1)/(addIr (- bS S1 1%g *: tau (chi - phi))). rewrite [in LHS]tau_chi_phi !scalerDr -!raddfZ_Cint ?rpredN ?Z_S1_1 //=. rewrite addrACA -!raddfD -raddfB !scalerDr !scaleNr scalerN !opprK. rewrite Dtau2/= ?Dtau1 ?zcharD1E ?cfunE; first by rewrite -raddfD addrACA. by rewrite mulrC subrr rpredB ?rpredZ_Cint ?Z_S1_1 /=. by rewrite mulrC bS2_1 -chi1_phi mulNr addNr rpredD ?rpredZ_Cint ?Z_S1_1 /=. 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 zmodp) mathcomp(gfunctor gproduct cyclic pgroup frobenius) mathcomp(matrix mxalgebra mxrepresentation vector ssrint) mathcomp(ssrnum algC classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4)