proposition: Lemma cfker_prTIres j : j != 0 -> ~~ (H \subset cfker (chi_ j)).
proof: Proof. rewrite -(cfRes_prTIirr _ 0) cfker_Res ?irr_char // subsetI sHK /=. apply: contra => kerHmu0j; rewrite -irr_eq1; apply/eqP/cfun_inP=> y W2y. have [[x W1x ntx] mulW] := (trivgPn _ ntW1, dprodW defW). rewrite cfun1E W2y -(cfDprodEr defW _ W1x W2y) -dprodr_IirrE -dprod_Iirr0l. have{ntx} W2'x: x \notin W2 by rewrite -[x \in W2]andTb -W1x -in_setI tiW12 inE. have V2xy: (x * y)%g \in W :\: W2 by rewrite inE -mulW mem_mulg ?groupMr ?W2'x. rewrite -[w_ 0 j](signrZK (primeTI_Isign ptiWL j)) cfunE -prTIirr_id //. have V2x: x \in W :\: W2 by rewrite inE W2'x (subsetP sW1W). rewrite cfkerMr ?(subsetP (subset_trans sW2H kerHmu0j)) ?prTIirr_id // cfunE. by rewrite signrMK -[x]mulg1 dprod_Iirr0l dprodr_IirrE cfDprodEr ?lin_char1. 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)