proposition: Theorem normedTI_prTIset : normedTI (W :\: W2) L W.
proof: Proof. have [[_ _ cW12 _] [_ _ nKW1 tiKW1]] := (dprodP defW, sdprodP defL). have nV2W: W \subset 'N(W :\: W2) by rewrite sub_abelian_norm ?subsetDl. have piW1_W: {in W1 & W2, forall x y, (x * y).`_\pi(W1) = x}. move=> x y W1x W2y /=; rewrite consttM /commute ?(centsP cW12 y) //. rewrite constt_p_elt ?(mem_p_elt _ W1x) ?pgroup_pi // (constt1P _) ?mulg1 //. by rewrite /p_elt -coprime_pi' // (coprimegS _ coW12) ?cycle_subG. have nzV2W: W :\: W2 != set0 by apply: contraNneq ntV; rewrite -subset0 => <-. apply/normedTI_memJ_P; split=> // xy g V2xy Lg. apply/idP/idP=> [| /(subsetP nV2W)/memJ_norm->//]. have{xy V2xy} [/(mem_dprod defW)[x [y [W1x W2y -> _]]] W2'xy] := setDP V2xy. have{W2'xy} ntx: x != 1%g by have:= W2'xy; rewrite groupMr // => /group1_contra. have{g Lg} [k [w [Kk /(subsetP sW1W)Ww -> _]]] := mem_sdprod defL Lg. rewrite conjgM memJ_norm ?(subsetP nV2W) ?(groupMr k) // => /setDP[Wxyk _]. have{Wxyk piW1_W} W1xk: x ^ k \in W1. have [xk [yk [W1xk W2yk Dxyk _]]] := mem_dprod defW Wxyk. by rewrite -(piW1_W x y) // -consttJ Dxyk piW1_W. rewrite (subsetP sW2W) // -(@prKW1 x) ?in_setD1 ?ntx // inE Kk /=. rewrite cent1C (sameP cent1P commgP) -in_set1 -set1gE -tiKW1 inE. by rewrite (subsetP _ _ (mem_commg W1x Kk)) ?commg_subr // groupM ?groupV. Qed.
imports: mathcomp.ssreflect.ssreflect mathcomp(ssrbool ssrfun eqtype ssrnat seq path div choice fintype) mathcomp(tuple finfun bigop order prime ssralg poly finset fingroup) mathcomp(morphism perm automorphism quotient action gfunctor gproduct) mathcomp(center commutator zmodp cyclic pgroup nilpotent hall frobenius) mathcomp(matrix mxalgebra mxrepresentation vector ssrnum algC classfun) mathcomp(character inertia vcharacter) odd_order(PFsection1 PFsection2 PFsection3)