proposition: Lemma mem_vecof u (V : {vspace vT}) : (vecof e u \in V) = (u <= msof V)%MS.
proof: Proof. apply/idP/submxP=> [|[v ->{u}]]; last by rewrite -hom_vecof// memv_proj. rewrite -[V in X in X -> _]msofK => /memv_imgP[v _]. by move=> /(canRL (vecofK _)) ->//; rewrite -rowmxof_mul//; eexists. Qed.
imports: mathcomp(all_ssreflect all_fingroup all_algebra all_solvable)