proposition: Lemma Wedderburn_subring_center i : ('Z('R_i) :=: mxvec 'e_i)%MS.
proof: Proof. have [nz_e Re ideR idRe] := Wedderburn_is_id i. have Ze: (mxvec 'e_i <= 'Z('R_i))%MS. rewrite sub_capmx [(_ <= _)%MS]Re. by apply/cent_mxP=> A R_A; rewrite ideR // idRe. pose irrG := socle_irr i; set rG := socle_repr i in irrG. pose E_G := enveloping_algebra_mx rG; have absG := splitG irrG. apply/eqmxP; rewrite andbC -(geq_leqif (mxrank_leqif_eq Ze)). have ->: \rank (mxvec 'e_i) = (0 + 1)%N. by apply/eqP; rewrite eqn_leq rank_leq_row lt0n mxrank_eq0 mxvec_eq0. rewrite -(mxrank_mul_ker _ (lin_mx (gring_op rG))) addnC leq_add //. rewrite leqn0 mxrank_eq0 -submx0 -(ker_irr_comp_op irrG) capmxS //. by rewrite irr_reprK capmxSl. apply: leq_trans (mxrankS _) (rank_leq_row (mxvec 1%:M)). apply/memmx_subP=> Ar; case/submxP=> a ->{Ar}. rewrite mulmxA mul_rV_lin /=; set A := vec_mx _. rewrite memmx1 (mx_abs_irr_cent_scalar absG) // -memmx_cent_envelop. apply/cent_mxP=> Br; rewrite -(irr_comp_envelop irrG) irr_reprK. case/submxP=> b /(canRL mxvecK) ->{Br}; rewrite mulmxA mx_rV_lin /=. set B := vec_mx _; have RiB: (B \in 'R_i)%MS by rewrite vec_mxK submxMl. have sRiR: ('R_i <= R_G)%MS by rewrite -Wedderburn_sum (sumsmx_sup i). have: (A \in 'Z('R_i))%MS by rewrite vec_mxK submxMl. rewrite sub_capmx => /andP[RiA /cent_mxP cRiA]. by rewrite -!gring_opM ?(memmx_subP sRiR) 1?cRiA. 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)