proposition: Lemma sub_aimgP (F0 : fieldType) (L L' : splittingFieldType F0) (iota : 'AHom(L, L')) (F : {subfield L'}) : reflect (exists E : {subfield L}, (iota @: E)%VS = F) (F <= iota @: fullv)%VS.
proof: Proof. apply: (iffP idP) => [Fiota|[E <-]]; last by rewrite limgS ?subvf. suff F_is_aspace : is_aspace (iota @^-1: F)%VS. by exists (ASpace F_is_aspace); apply/eqP; rewrite eqEsubv/= lpreimK ?subvv. apply/andP => /=; split. by apply/has_algid1; rewrite -memv_preim rmorph1 rpred1. by apply/prodvP => u v; rewrite -!memv_preim => uF vF; rewrite rmorphM rpredM. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)