proposition: Lemma Clifford_rstabs_simple (W : sH) : mxsimple (subg_repr rG (rstabs_sub rG W)) W.
proof: Proof. split => [||U modU sUW nzU]; last 2 [exact: nz_socle]. by rewrite /mxmodule rstabs_subg setIid. have modUH: mxmodule rH U. apply/mxmoduleP=> h Hh; rewrite (mxmoduleP modU) //. rewrite /= -Clifford_astab1 !(inE, sub1set) (subsetP sHG) //. rewrite (astab_act (subsetP Clifford_astab h _)) ?inE //=. by rewrite mem_gen // inE Hh. apply: (mxsimple_exists modUH nzU) => [[M simM sMU]]. have [t [x_ /(_ W)[Gx_ defW _]]] := Clifford_component_basis simM. rewrite -defW; apply/sumsmx_subP=> j _; set x := x_ W j. have{Gx_} Gx: x \in G by rewrite Gx_. apply: submx_trans (submxMr _ sMU) _; apply: (mxmoduleP modU). rewrite inE -val_Clifford_act Gx //; set Wx := 'Cl%act W x. case: (eqVneq Wx W) (simM) => [-> //=|] neWxW [_ /negP[]]; rewrite -submx0. rewrite (canF_eq (actKin 'Cl Gx)) in neWxW. rewrite -(component_mx_disjoint _ _ neWxW); try exact: socle_simple. rewrite sub_capmx {1}(submx_trans sMU sUW) val_Clifford_act ?groupV //. by rewrite -(eqmxMr _ defW) sumsmxMr (sumsmx_sup j) ?repr_mxK. 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)