proposition: Lemma normedTI_J x A G L : normedTI (A :^ x) (G :^ x) (L :^ x) = normedTI A G L.
proof: Proof. rewrite {1}/normedTI normJ -conjIg -(conj0g x) !(can_eq (conjsgK x)). congr [&& _, _ == _ & _]; rewrite /cover (reindex_inj (@conjsg_inj _ x)). by apply: eq_big => Hy; rewrite ?orbit_conjsg ?cardJg. by rewrite bigcupJ cardJg (eq_bigl _ _ (orbit_conjsg _ _ _ _)). Qed.
imports: mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat div) mathcomp(fintype bigop prime finset fingroup morphism) mathcomp(perm action quotient gproduct cyclic center) mathcomp(pgroup nilpotent sylow hall abelian)