proposition: Lemma prDade_sub2_TIirr i j : tau (delta_ j *: mu2_ i j - delta_ j *: mu2_ 0 j - mu2_ i 0 + mu2_ 0 0) = eta_ i j - eta_ 0 j - eta_ i 0 + eta_ 0 0.
proof: Proof. pose V0 := class_support V L; have sVV0: V \subset V0 := sub_class_support L V. have sV0A0: V0 \subset A0 by rewrite defA0 subsetUr. have nV0L: L \subset 'N(V0) := class_support_norm V L. have [_ _ /normedTI_memJ_P[ntV _ tiV]] := ctiWG. have [/andP[sA0L _] _ A0'1 _ _] := ddA0. have{sA0L A0'1} sV0G: V0 \subset G^#. by rewrite (subset_trans sV0A0) // subsetD1 A0'1 (subset_trans sA0L). have{sVV0} ntV0: V0 != set0 by apply: contraNneq ntV; rewrite -subset0 => <-. have{ntV} tiV0: normedTI V0 G L. apply/normedTI_memJ_P; split=> // _ z /imset2P[u y Vu Ly ->] Gz. apply/idP/idP=> [/imset2P[u1 y1 Vu1 Ly1 Duyz] | Lz]; last first. by rewrite -conjgM imset2_f ?groupM. rewrite -[z](mulgKV y1) groupMr // -(groupMl _ Ly) (subsetP sWL) //. by rewrite -(tiV u) ?groupM ?groupV // ?(subsetP sLG) // !conjgM Duyz conjgK. have{ntV0 sV0A0 nV0L tiV0} DtauV0: {in 'CF(L, V0), tau =1 'Ind}. by move=> beta V0beta; rewrite /= -(restr_DadeE _ sV0A0) //; apply: Dade_Ind. pose alpha := cfCyclicTIset defW i j; set beta := _ *: mu2_ i j - _ - _ + _. have Valpha: alpha \in 'CF(W, V) := cfCycTI_on ctiWL i j. have Dalpha: alpha = w_ i j - w_ 0 j - w_ i 0 + w_ 0 0. by rewrite addrC {1}cycTIirr00 addrA addrAC addrA addrAC -cfCycTI_E. rewrite -!(linearB sigma) -linearD -Dalpha cycTIiso_Ind //. suffices ->: beta = 'Ind[L] alpha by rewrite DtauV0 ?cfInd_on ?cfIndInd. rewrite Dalpha -addrA -[w_ 0 0]opprK -opprD linearB /= /beta -scalerBr. by rewrite !(cfInd_sub_prTIirr ptiWL) prTIsign0 scale1r opprD opprK addrA. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg poly finset fingroup) mathcomp(morphism perm automorphism quotient action gfunctor gproduct) mathcomp(center commutator zmodp cyclic pgroup nilpotent hall frobenius) mathcomp(matrix mxalgebra mxrepresentation vector ssrnum algC classfun) mathcomp(character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3)