proposition: Lemma FTsupp0_typeP M (H := M`_\F) U W1 W2 W (defW : W1 \x W2 = W) : M \in 'M -> of_typeP M U defW -> let V := W :\: (W1 :|: W2) in 'A0(M) :\: 'A(M) = class_support V M.
proof: Proof. move: W1 W2 => K Ks in defW * => maxM MtypeP /=. have [[_ _ ntK _] _ _ _ _] := MtypeP. have [PmaxM hallK defKs _ _] := typePfacts maxM MtypeP. have [[_ sHMs _ _] _] := Fcore_structure maxM. have [V complV] := ex_kappa_compl maxM hallK. have [[_ [_ _ sKsH _] _] _ [_ [-> _] _ _]] := BGsummaryC maxM complV ntK. by rewrite -(setIidPr sKsH) setIA (setIidPl sHMs) defKs -(dprodWY defW). Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq div path fintype) mathcomp(bigop finset prime fingroup morphism perm automorphism quotient) mathcomp(action gproduct gfunctor pgroup cyclic center commutator) mathcomp(gseries nilpotent sylow abelian maximal hall frobenius) odd_order(BGsection1 BGsection2 BGsection3 BGsection4 BGsection5) odd_order(BGsection6 BGsection7 BGsection9 BGsection10 BGsection12) odd_order(BGsection13 BGsection14 BGsection15)