proposition: Lemma FTtype1_seqInd_ortho L1 L2 (maxL1 : L1 \in 'M) (maxL2 : L2 \in 'M) (L1type1 : FTtype L1 == 1%N) (L2type1 : FTtype L2 == 1%N) (H1 := L1`_\F%G) (H2 := L2`_\F%G) (calS1 := seqIndD H1 L1 H1 1) (calS2 := seqIndD H2 L2 H2 1) (R1 := sval (Rgen maxL1 L1type1)) (R2 := sval (Rgen maxL2 L2type1)) : gval L2 \notin L1 :^: G -> {in calS1 & calS2, forall chi1 chi2, orthogonal (R1 chi1) (R2 chi2)}.
proof: Proof. move=> notL1G_L2; without loss{notL1G_L2} disjointA1A: L1 L2 maxL1 maxL2 L1type1 L2type1 @H1 @H2 @calS1 @calS2 @R1 @R2 / [disjoint 'A1~(L2) & 'A~(L1)]. - move=> IH_L; have [_ _] := FT_Dade_support_disjoint maxL1 maxL2 notL1G_L2. by case=> /IH_L-oS12 chi1 chi2 *; first rewrite orthogonal_sym; apply: oS12. case: (Rgen _ _) @R1 => /= R1; set R1' := sval _ => [[subcoh1 hR1' defR1]]. case: (Rgen _ _) @R2 => /= R2; set R2' := sval _ => [[subcoh2 hR2' defR2]]. pose tau1 := FT_Dade maxL1; pose tau2 := FT_Dade maxL2. move=> chi1 chi2 calS1_chi1 calS2_chi2. have [_ _ _ /(_ chi1 calS1_chi1)[Z_R1 o1R1 dtau1_chi1] _] := subcoh1. have{o1R1} [uR1 oR1] := orthonormalP o1R1. apply/orthogonalP=> a b R1a R2b; pose psi2 := tau2 (chi2 - chi2^*%CF). have Z1a: a \in dirr G by rewrite dirrE Z_R1 //= oR1 ?eqxx. suffices{b R2b}: '[a, psi2] == 0. apply: contraTeq => nz_ab; rewrite /psi2 /tau2. have [_ _ _ /(_ chi2 calS2_chi2)[Z_R2 o1R2 ->] _] := subcoh2. suffices [e ->]: {e | a = if e then - b else b}. rewrite -scaler_sign cfdotC cfdotZr -cfdotZl scaler_sumr. by rewrite cfproj_sum_orthonormal // conjCK signr_eq0. have [_ oR2] := orthonormalP o1R2. have Z1b: b \in dirr G by rewrite dirrE Z_R2 //= oR2 ?eqxx. move/eqP: nz_ab; rewrite cfdot_dirr //. by do 2?[case: eqP => [-> | _]]; [exists true | exists false | ]. have [chi1D _ Achi1] := FTtype1_seqInd_facts maxL1 L1type1 calS1_chi1. pose S_chi1 := [set i0 in irr_constt chi1]. pose bchi i := 'chi[_ : {set gT}]_i - ('chi_i)^*%CF. have [t S_chi1t et]: exists2 t, t \in S_chi1 & tau1 (bchi _ t) = a - a^*%CF. suffices: ~~ [forall i in S_chi1, '[tau1 (bchi L1 i), a] <= 0]. rewrite negb_forall_in => /exists_inP[i Si tau1i_a]; exists i => //. case/dIrrP: Z1a tau1i_a => ia ->. have [k ->]: exists k, tau1 (bchi _ i) = bchi G k. exact: Dade_irr_sub_conjC (mem_irr _) (Achi1 i Si). have {1}->: bchi G k = dchi (false, k) + dchi (true, conjC_Iirr k). by rewrite /dchi !scaler_sign conjC_IirrE. rewrite cfdotDl !cfdot_dchi addrACA -opprD subr_le0 -!natrD leC_nat. do 2?case: (_ =P ia) => [<-|] _ //; first by rewrite /dchi scale1r. by rewrite /dchi scaleN1r conjC_IirrE rmorphN /= cfConjCK opprK addrC. have: '[tau1 (chi1 - chi1^*%CF), a] == 1. rewrite /tau1 dtau1_chi1 (bigD1_seq a) //= cfdotDl cfdot_suml oR1 // eqxx. by rewrite big1_seq ?addr0 // => xi /andP[/negPf a'xi ?]; rewrite oR1 ?a'xi. apply: contraL => /forall_inP tau1a_le0. rewrite (lt_eqF (le_lt_trans _ ltr01)) // chi1D rmorph_sum /= -/S_chi1. rewrite -sumrB [tau1 _]linear_sum /= -/tau1 cfdot_suml. by rewrite -oppr_ge0 -sumrN sumr_ge0 // => i /tau1a_le0; rewrite oppr_ge0. clear Achi1 dtau1_chi1 uR1 defR1. suffices: '[a, psi2] == - '[a, psi2] by rewrite -addr_eq0 (mulrn_eq0 _ 2). have A1bchi2: chi2 - (chi2^*)%CF \in 'Z[calS2, 'A1(L2)]. by rewrite FTsupp1_type1 // seqInd_sub_aut_zchar ?gFnormal. have{t S_chi1t et} /eqP{2}->: '[a, psi2] == '[a^*%CF, psi2]. move/zchar_on in A1bchi2; rewrite -subr_eq0 -cfdotBl. rewrite [psi2]FT_DadeE ?(cfun_onS (FTsupp1_sub _)) // -FT_Dade1E // -et. rewrite (cfdot_complement (Dade_cfunS _ _)) ?(cfun_onS _ (Dade_cfunS _ _)) //. by rewrite FT_Dade_supportE FT_Dade1_supportE setTD -disjoints_subset. rewrite -2!raddfN opprB /= cfdot_conjCl -Dade_conjC rmorphB /= cfConjCK -/tau2. rewrite conj_Cint ?Cint_cfdot_vchar ?(Z_R1 a) // Dade_vchar //. rewrite (zchar_onS (FTsupp1_sub _)) // (zchar_sub_irr _ A1bchi2) //. exact: seqInd_vcharW. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice) mathcomp(fintype tuple finfun bigop order prime ssralg 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 mxpoly mxrepresentation mxabelem vector) mathcomp(falgebra fieldext finfield) odd_order(BGsection1 BGsection2 BGsection3 BGsection4 BGsection7) odd_order(BGsection14 BGsection15 BGsection16) mathcomp(ssrnum ssrint algC cyclotomic algnum) mathcomp(classfun character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3 PFsection4 PFsection5) odd_order(PFsection6 PFsection7 PFsection8 PFsection9 PFsection10) odd_order(PFsection11)