proposition: Lemma classg_base_center : (classg_base :=: 'Z(R_G))%MS.
proof: Proof. apply/eqmxP/andP; split. apply/row_subP=> k; rewrite rowK /gset_mx sub_capmx {1}linear_sum. have [x Gx ->{k}] := imsetP (enum_valP k); have sxGG := groupCl Gx. rewrite summx_sub => [|y xGy]; last by rewrite envelop_mx_id ?sxGG. rewrite memmx_cent_envelop; apply/centgmxP=> y Gy. rewrite {2}(reindex_acts 'J _ Gy) ?astabsJ ?class_norm //=. rewrite mulmx_suml mulmx_sumr; apply: eq_bigr => z; move/sxGG=> Gz. by rewrite -!repr_mxM ?groupJ -?conjgC. apply/memmx_subP=> A; rewrite sub_capmx memmx_cent_envelop. case/andP=> /envelop_mxP[a ->{A}] cGa. rewrite (partition_big_imset (class^~ G)) -/(classes G) /=. rewrite linear_sum summx_sub //= => xG GxG; have [x Gx def_xG] := imsetP GxG. apply: submx_trans (scalemx_sub (a x) (submx_refl _)). rewrite (eq_row_sub (enum_rank_in GxG xG)) // linearZ /= rowK enum_rankK_in //. rewrite !linear_sum {xG GxG}def_xG; apply: eq_big => [y | xy] /=. apply/idP/andP=> [| [_ xGy]]; last by rewrite -(eqP xGy) class_refl. by case/imsetP=> z Gz ->; rewrite groupJ // classGidl. case/imsetP=> y Gy ->{xy}; rewrite linearZ; congr (_ *: _). move/(canRL (repr_mxK aG Gy)): (centgmxP cGa y Gy); have Gy' := groupVr Gy. move/(congr1 (gring_proj x)); rewrite -mulmxA mulmx_suml !linear_sum. rewrite (bigD1 x Gx) big1 => [|z /andP[Gz]]; rewrite !linearZ /=; last first. by rewrite eq_sym gring_projE // => /negPf->; rewrite scaler0. rewrite gring_projE // eqxx scalemx1 (bigD1 (x ^ y)%g) ?groupJ //=. rewrite big1 => [|z /andP[Gz]]; rewrite -scalemxAl !linearZ /=. rewrite !addr0 -!repr_mxM ?groupM // mulgA mulKVg mulgK => /rowP/(_ 0). by rewrite gring_projE // eqxx scalemx1 !mxE. rewrite eq_sym -(can_eq (conjgKV y)) conjgK conjgE invgK. by rewrite -!repr_mxM ?gring_projE ?groupM // => /negPf->; rewrite scaler0. 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)