proposition: Lemma rfix_abelem (H : {set gT}) : H \subset G -> (rfix_mx rG H :=: rowg_mx (ErV @* 'C_E(H)%g))%MS.
proof: Proof. move/subsetP=> sHG; apply/eqmxP/andP; split. rewrite -rowgS rowg_mxK -sub_rVabelem_im // subsetI sub_rVabelem /=. apply/centsP=> y /morphimP[v _] /[1!inE] cGv ->{y} x Gx. by apply/commgP/conjg_fixP; rewrite /= -rVabelemJ ?sHG ?(rfix_mxP H _). rewrite genmxE; apply/rfix_mxP=> x Hx; apply/row_matrixP=> i. rewrite row_mul rowK; case/morphimP: (enum_valP i) => z Ez /setIP[_ cHz] ->. by rewrite -abelem_rV_J ?sHG // conjgE (centP cHz) ?mulKg. Qed.
imports: HB(structures) mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq path) mathcomp(div choice fintype tuple finfun bigop prime) mathcomp(ssralg poly finset fingroup morphism perm) mathcomp(automorphism quotient gproduct action finalg) mathcomp(zmodp commutator cyclic center pgroup gseries) mathcomp(nilpotent sylow maximal abelian matrix) mathcomp(mxalgebra mxrepresentation)