proposition: Lemma aimg_normalClosure (F0 : fieldType) (L L' : splittingFieldType F0) (iota : 'AHom(L, L')) (K E : {subfield L}) : (iota @: normalClosure K E)%VS = normalClosure (iota @: K) (iota @: E).
proof: Proof. set M' := normalClosure (iota @: _) _; have iK0 := AHom_lker0 iota. have M'sub : (M' <= iota @: normalClosure K E)%VS. by rewrite normalClosureP ?limgS//= normalField_aimg/=. apply/eqP; rewrite eqEsubv M'sub /M'. have /sub_aimgP[/= M ME] : (M' <= iota @: fullv)%VS. by apply: subv_trans M'sub _; rewrite limgS ?subvf. have KM : (K <= M)%VS by rewrite -(limg_ker0 _ _ iK0) ME/= normalClosureSl. rewrite -ME limgS// normalClosureP//. by rewrite -(limg_ker0 _ _ iK0) ME/= normalClosureSr. by rewrite -(normalField_aimg iota)// ME// normalClosure_normal. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)