proposition: Corollary coherent_ortho_supp S1 chi (tau1 : {additive 'CF(L) -> 'CF(G)}) : cfConjC_subset S1 S -> coherent_with S1 L^# tau tau1 -> chi \in S -> chi \notin S1 -> orthogonal (map tau1 S1) (R chi).
proof: Proof. move=> uccS1 cohS1 Schi S1'chi; have [uS1 sS1S ccS1] := uccS1. apply/orthogonalP=> _ mu /mapP[phi S1phi ->] Rmu; have Sphi := sS1S _ S1phi. have [e /mem_subseq Re ->] := mem_coherent_sum_subseq uccS1 cohS1 S1phi. rewrite cfdot_suml big1_seq // => xi {e}/Re Rxi. apply: orthogonalP xi mu Rxi Rmu; have [_ _ _ _ -> //] := cohS. rewrite /orthogonal /= !andbT cfdot_conjCr fmorph_eq0. by rewrite !(orthoPr (subset_ortho_subcoherent sS1S _ _)) ?ccS1 ?eqxx. 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)