proposition: Lemma ker_irr_comp_op : ('R_iG :&: kermx (lin_mx (gring_op rG)))%MS = 0.
proof: Proof. apply/eqP; rewrite -submx0; apply/memmx_subP=> A. rewrite sub_capmx /= submx0 mxvec_eq0 => /andP[R_A]. rewrite (sameP sub_kermxP eqP) mul_vec_lin mxvec_eq0 /= => opA0. have [_ Re ideR _] := Wedderburn_is_id iG; rewrite -[A]ideR {ideR}//. move: Re; rewrite genmxE mem_sub_gring /socle_val => /andP[Re]. rewrite -{2}(gring_rowK Re) -submx0. pose simMi := socle_simple iG; have [J [M isoM ->]] := component_mx_def simMi. case/sub_sumsmxP=> e ->; rewrite linear_sum mulmx_suml summx_sub // => j _. rewrite -(in_submodK (submxMl _ (M j))); move: (in_submod _ _) => v. have modMj: mxmodule aG (M j) by apply: mx_iso_module (isoM j) _; case: simMi. have rsimMj: mx_rsim rG (submod_repr modMj). by apply: mx_rsim_trans rsim_irr_comp _; apply/mx_rsim_iso. have [f [f' _ hom_f]] := mx_rsim_def (mx_rsim_sym rsimMj); rewrite submx0. have <-: (gring_mx aG (val_submod (v *m (f *m gring_op rG A *m f')))) = 0. by rewrite (eqP opA0) !(mul0mx, linear0). have: (A \in R_G)%MS by rewrite -Wedderburn_sum (sumsmx_sup iG). case/envelop_mxP=> a ->; rewrite !(linear_sum, mulmx_suml) /=; apply/eqP. apply: eq_bigr=> x Gx; rewrite !linearZ -scalemxAl !linearZ /=. by rewrite gring_opG // -hom_f // val_submodJ // gring_mxJ. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly polydiv finset fingroup morphism) mathcomp(perm automorphism quotient finalg action zmodp) mathcomp(commutator cyclic center pgroup matrix mxalgebra) mathcomp(mxpoly)