proposition: Lemma prTIirr0P k : reflect (exists i, 'chi_k = mu2_ i 0) (K \subset cfker 'chi_k).
proof: Proof. suff{k}: [set k | K \subset cfker 'chi_k] == [set Imu2 (i, 0) | i : Iirr W1]. move/eqP/setP/(_ k); rewrite inE => ->. by apply: (iffP imsetP) => [[i _]|[i /irr_inj]] ->; exists i. have [isoW1 abW1] := (sdprod_isog defL, cyclic_abelian cycW1). have abLbar: abelian (L / K) by rewrite -(isog_abelian isoW1). rewrite eqEcard andbC card_imset ?nirrW1 => [| i1 i2 /prTIirr_inj[] //]. rewrite [w1](card_isog isoW1) -card_Iirr_abelian //. rewrite -(card_image (can_inj (mod_IirrK nsKL))) subset_leq_card; last first. by apply/subsetP=> _ /imageP[k1 _ ->]; rewrite inE mod_IirrE ?cfker_mod. apply/subsetP=> k; rewrite inE => kerKk. have /irrP[ij DkW]: 'Res 'chi_k \in irr W. rewrite lin_char_irr ?cfRes_lin_char // lin_irr_der1. by apply: subset_trans kerKk; rewrite der1_min ?normal_norm. have{ij DkW} [i DkW]: exists i, 'Res 'chi_k = w_ i 0. have /codomP[[i j] Dij] := dprod_Iirr_onto defW ij; exists i. rewrite DkW Dij; congr (w_ i _); apply/eqP; rewrite -subGcfker. rewrite -['chi_j](cfDprodKr_abelian defW i) // -dprod_IirrE -{}Dij -{}DkW. by rewrite cfResRes // sub_cfker_Res // (subset_trans sW2K kerKk). apply/imsetP; exists i => //=; apply/irr_inj. suffices ->: 'chi_k = delta_ 0 *: mu2_ i 0 by rewrite prTIsign0 scale1r. rewrite -cycTIiso_prTIirr -(eq_in_cycTIiso _ (irr_dirr k)) // => x /setDP[Wx _]. by rewrite -/(w_ i 0) -DkW cfResE. 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)