proposition: Lemma cfdot_sum_dchi (phi1 phi2 : 'CF(G)) : '[\sum_(i in dirr_constt phi1) dchi i, \sum_(i in dirr_constt phi2) dchi i] = #|dirr_constt phi1 :&: dirr_constt phi2|%:R - #|dirr_constt phi1 :&: dirr_constt (- phi2)|%:R.
proof: Proof. rewrite addrC (big_setID (dirr_constt (- phi2))) /= cfdotDl; congr (_ + _). rewrite cfdot_suml -sumr_const -sumrN; apply: eq_bigr => i /setIP[p1i p2i]. rewrite cfdot_sumr (bigD1 (ndirr i)) -?dirr_constt_oppr //= dchi_ndirrE. rewrite cfdotNr cfnorm_dchi big1 ?addr0 // => j /andP[p2j i'j]. rewrite cfdot_dchi -(inv_eq ndirrK) [in rhs in - rhs]eq_sym (negPf i'j) subr0. rewrite (negPf (contraTneq _ p2i)) // => ->. by rewrite dirr_constt_oppr dirr_constt_oppl. rewrite cfdot_sumr (big_setID (dirr_constt phi1)) setIC /= addrC. rewrite big1 ?add0r => [|j /setDP[p2j p1'j]]; last first. rewrite cfdot_suml big1 // => i /setDP[p1i p2'i]. rewrite cfdot_dchi (negPf (contraTneq _ p1i)) => [|-> //]. rewrite (negPf (contraNneq _ p2'i)) ?subrr // => ->. by rewrite dirr_constt_oppr ndirrK. rewrite -sumr_const; apply: eq_bigr => i /setIP[p1i p2i]; rewrite cfdot_suml. rewrite (bigD1 i) /=; last by rewrite inE dirr_constt_oppr dirr_constt_oppl. rewrite cfnorm_dchi big1 ?addr0 // => j /andP[/setDP[p1j _] i'j]. rewrite cfdot_dchi (negPf i'j) (negPf (contraTneq _ p1j)) ?subrr // => ->. exact: dirr_constt_oppl. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime order) mathcomp(ssralg poly finset fingroup morphism perm) mathcomp(automorphism quotient finalg action gproduct) mathcomp(zmodp commutator cyclic center pgroup sylow) mathcomp(frobenius vector ssrnum ssrint archimedean intdiv) mathcomp(algC algnum classfun character integral_char)