proposition: Lemma normalField_aimg (K : {subfield L}) : (K <= E)%VS -> normalField (iota @: K) (iota @: E) = normalField K E.
proof: Proof. move=> KE; have iotaKS : (iota @: K <= iota @: E)%VS by rewrite limgS. apply/splitting_normalField/splitting_normalField => //= -[p pK [rs peq Krs]]. have /polyOver_aimg [q qK pE] := pK. have /subset_limgP [rs' _ rsE] : {subset rs <= (iota @: E)%VS}. by rewrite -Krs; apply/seqv_sub_adjoin. exists q => //; exists rs'. by have := peq; rewrite pE rsE -map_prod_XsubC/= eqp_map. by do [rewrite rsE -aimg_adjoin_seq => /eqP; rewrite eq_limg_ker0// => /eqP] in Krs. exists (map_poly iota p) => //; first by rewrite mapf_polyOver. by apply/splittingFieldFor_aimg; exists rs. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra) mathcomp(all_solvable all_field) Abel(various char0)