proposition: Lemma lpreimK f W : (W <= limg f)%VS -> (f @: (f @^-1: W))%VS = W.
proof: Proof. move=> sWf; rewrite limgD (capv_idPl sWf) // -limg_comp. have /eqP->: (f @: lker f == 0)%VS by rewrite -lkerE. have /andP[/eqP defW _] := vbasisP W; rewrite addv0 -defW limg_span. rewrite map_id_in // => x Xx; rewrite lfunE /= limg_lfunVK //. by apply: span_subvP Xx; rewrite defW. Qed.
imports: HB(structures) mathcomp(ssreflect ssrfun ssrbool eqtype ssrnat seq choice) mathcomp(fintype bigop finfun tuple) mathcomp(ssralg matrix mxalgebra zmodp)