proposition: Lemma der1_stab_Ohm1_SCN_series : ('C(Z) :&: 'C_G(A / Z | 'Q))^`(1) \subset A.
proof: Proof. case/SCN_P: SCN_A => /andP[sAG nAG] {4} <-. rewrite subsetI {1}setICA comm_subG ?subsetIl //= gen_subG. apply/subsetP=> w /imset2P[u v]. rewrite -groupV -(groupV _ v) /= astabQR //= -/Z !inE groupV. case/and4P=> cZu _ _ sRuZ /and4P[cZv' _ _ sRvZ] ->{w}. apply/centP=> a Aa; rewrite /commute -!mulgA (commgCV v) (mulgA u). rewrite (centP cZu); last by rewrite (subsetP sRvZ) ?mem_commg ?set11 ?groupV. rewrite 2!(mulgA v^-1) mulKVg 4!mulgA invgK (commgC u^-1) mulgA. rewrite -(mulgA _ _ v^-1) -(centP cZv') ?(subsetP sRuZ) ?mem_commg ?set11//. by rewrite -!mulgA invgK mulKVg !mulKg. Qed.
imports: mathcomp(ssreflect ssrbool ssrfun eqtype ssrnat seq choice) mathcomp(div fintype finfun bigop finset prime binomial) mathcomp(fingroup morphism perm automorphism quotient) mathcomp(action commutator gproduct gfunctor ssralg) mathcomp(countalg finalg zmodp cyclic pgroup center gseries) mathcomp(nilpotent sylow abelian finmodule)