proposition: Lemma lker0_img_cap (K : fieldType) (aT rT : vectType K) (f : 'Hom(aT, rT)) (U V : {vspace aT}) : lker f == 0%VS -> (f @: (U :&: V) = f @: U :&: f @: V)%VS.
proof: Proof. move=> kf0; apply/eqP; rewrite eqEsubv limg_cap/=; apply/subvP => x. rewrite memv_cap => /andP[/memv_imgP[u uU ->]] /memv_imgP[v vV]. by move=> /(lker0P kf0) eq_uv; rewrite memv_img// memv_cap uU eq_uv vV. Qed.
imports: HB(structures) mathcomp(all_ssreflect all_fingroup all_algebra all_solvable) mathcomp(all_field)