proposition: Lemma Wedderburn_min_ideal m i (E : 'A_(m, nG)) : E != 0 -> (E <= 'R_i)%MS -> mx_ideal R_G E -> (E :=: 'R_i)%MS.
proof: Proof. move=> nzE sE_Ri /andP[idlE idrE]; apply/eqmxP; rewrite sE_Ri. pose M := E *m pinvmx R_G; have defE: E = M *m R_G. by rewrite mulmxKpV // (submx_trans sE_Ri) // genmxE submxMl. have modM: mxmodule aG M by rewrite regular_module_ideal -defE. have simSi := socle_simple i; set Si := socle_base i in simSi. have [I [W isoW defW]]:= component_mx_def simSi. rewrite /'R_i /socle_val /= defW genmxE defE submxMr //. apply/sumsmx_subP=> j _. have simW := mx_iso_simple (isoW j) simSi; have [modW _ minW] := simW. have [{minW}dxWE | nzWE] := eqVneq (W j :&: M)%MS 0; last first. by rewrite (sameP capmx_idPl eqmxP) minW ?capmxSl ?capmx_module. have [_ Rei ideRi _] := Wedderburn_is_id i. have:= nzE; rewrite -submx0 => /memmx_subP[A E_A]. rewrite -(ideRi _ (memmx_subP sE_Ri _ E_A)). have:= E_A; rewrite defE mem_sub_gring => /andP[R_A M_A]. have:= Rei; rewrite genmxE mem_sub_gring => /andP[Re]. rewrite -{2}(gring_rowK Re) /socle_val defW => /sub_sumsmxP[e ->]. rewrite !(linear_sum, mulmx_suml) summx_sub //= => k _. rewrite -(gring_rowK R_A) -gring_mxA -mulmxA gring_rowK //. rewrite ((W k *m _ =P 0) _) ?linear0 ?sub0mx //. have [f _ homWf defWk] := mx_iso_trans (mx_iso_sym (isoW j)) (isoW k). rewrite -submx0 -{k defWk}(eqmxMr _ defWk) -(hom_envelop_mxC homWf) //. rewrite -(mul0mx _ f) submxMr {f homWf}// -dxWE sub_capmx. rewrite (mxmodule_envelop modW) //=; apply/row_subP=> k. rewrite row_mul -mem_gring_mx -(gring_rowK R_A) gring_mxA gring_rowK //. by rewrite -defE (memmx_subP idlE) // mem_mulsmx ?gring_mxP. 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)