proposition: Lemma rsim_irr_comp : mx_rsim rG (irr_repr iG).
proof: Proof. have [M [modM rsimM]] := rsim_regular_submod irrG F'G. have simM: mxsimple aG M. case/mx_irrP: irrG => n_gt0 minG. have [f def_n injf homf] := mx_rsim_sym rsimM. apply/(submod_mx_irr modM)/mx_irrP. split=> [|U modU nzU]; first by rewrite def_n. rewrite /row_full -(mxrankMfree _ injf) -genmxE {4}def_n. apply: minG; last by rewrite -mxrank_eq0 genmxE mxrankMfree // mxrank_eq0. rewrite (eqmx_module _ (genmxE _)); apply/mxmoduleP=> x Gx. by rewrite -mulmxA -homf // mulmxA submxMr // (mxmoduleP modU). pose i := PackSocle (component_socle sG simM). have{modM} rsimM: mx_rsim rG (socle_repr i). apply: mx_rsim_trans rsimM (mx_rsim_sym _); apply/mx_rsim_iso. apply: (component_mx_iso (socle_simple _)) => //. by rewrite [component_mx _ _]PackSocleK component_mx_id. have [<- // | ne_i_iG] := eqVneq i iG. suffices {i M simM ne_i_iG rsimM}: gring_op rG 'e_iG != 0. by rewrite (not_rsim_op0 rsimM ne_i_iG) ?Wedderburn_id_mem ?eqxx. rewrite /iG; case: pickP => //= G0. suffices: rG 1%g == 0. by case/idPn; rewrite -mxrank_eq0 repr_mx1 mxrank1 -lt0n; case/mx_irrP: irrG. rewrite -gring_opG // repr_mx1 -Wedderburn_sum_id linear_sum big1 // => j _. by move/eqP: (G0 j). 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)