proposition: Lemma vchar_orthonormalP S : {subset S <= 'Z[irr G]} -> reflect (exists I : {set Iirr G}, exists b : Iirr G -> bool, perm_eq S [seq (-1) ^+ b i *: 'chi_i | i in I]) (orthonormal S).
proof: Proof. move=> vcS; apply: (equivP orthonormalP). split=> [[uniqS oSS] | [I [b defS]]]; last first. split=> [|xi1 xi2]; rewrite ?(perm_mem defS). rewrite (perm_uniq defS) map_inj_uniq ?enum_uniq // => i j /eqP. by rewrite eq_signed_irr => /andP[_ /eqP]. case/mapP=> [i _ ->] /mapP[j _ ->]; rewrite eq_signed_irr. rewrite cfdotZl cfdotZr rmorph_sign mulrA cfdot_irr -signr_addb mulr_natr. by rewrite mulrb andbC; case: eqP => //= ->; rewrite addbb eqxx. pose I := [set i | ('chi_i \in S) || (- 'chi_i \in S)]. pose b i := - 'chi_i \in S; exists I, b. apply: uniq_perm => // [|xi]. rewrite map_inj_uniq ?enum_uniq // => i j /eqP. by rewrite eq_signed_irr => /andP[_ /eqP]. apply/idP/mapP=> [Sxi | [i Ii ->{xi}]]; last first. move: Ii; rewrite mem_enum inE orbC -/(b i). by case b_i: (b i); rewrite (scale1r, scaleN1r). have: '[xi] = 1 by rewrite oSS ?eqxx. have vc_xi := vcS _ Sxi; rewrite cfdot_sum_irr. case/natr_sum_eq1 => [i _ | i [_ /eqP norm_xi_i xi_i'_0]]. by rewrite -normCK rpredX // natr_norm_int ?Cint_cfdot_vchar_irr. suffices def_xi: xi = (-1) ^+ b i *: 'chi_i. exists i; rewrite // mem_enum inE -/(b i) orbC. by case: (b i) def_xi Sxi => // ->; rewrite scale1r. move: Sxi; rewrite [xi]cfun_sum_cfdot (bigD1 i) //. rewrite big1 //= ?addr0 => [|j ne_ji]; last first. apply/eqP; rewrite scaler_eq0 -normr_eq0 -[_ == 0](expf_eq0 _ 2) normCK. by rewrite xi_i'_0 ?eqxx. have:= norm_xi_i; rewrite (aut_intr _ (Cint_cfdot_vchar_irr _ _)) //. rewrite -subr_eq0 subr_sqr_1 mulf_eq0 subr_eq0 addr_eq0 /b scaler_sign. case/pred2P=> ->; last by rewrite scaleN1r => ->. rewrite scale1r => Sxi; case: ifP => // SNxi. have:= oSS _ _ Sxi SNxi; rewrite cfdotNr cfdot_irr eqxx; case: eqP => // _. by move/eqP; rewrite oppr_eq0 oner_eq0. 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)