Theorem imlmhm

Description: The image of a vector space homomorphism is a vector space itself. (Contributed by Thierry Arnoux, 7-May-2023)

	Ref	Expression
Hypothesis	imlmhm.i	|- I = ( U |`s ran F )
Assertion	imlmhm	|- ( ( V e. LVec /\ F e. ( V LMHom U ) ) -> I e. LVec )

Proof

Step	Hyp	Ref	Expression
1		imlmhm.i	|- I = ( U |`s ran F )
2		lmhmlvec2	|- ( ( V e. LVec /\ F e. ( V LMHom U ) ) -> U e. LVec )
3		lmhmrnlss	|- ( F e. ( V LMHom U ) -> ran F e. ( LSubSp ` U ) )
4	3	adantl	|- ( ( V e. LVec /\ F e. ( V LMHom U ) ) -> ran F e. ( LSubSp ` U ) )
5		eqid	|- ( LSubSp ` U ) = ( LSubSp ` U )
6	1 5	lsslvec	|- ( ( U e. LVec /\ ran F e. ( LSubSp ` U ) ) -> I e. LVec )
7	2 4 6	syl2anc	|- ( ( V e. LVec /\ F e. ( V LMHom U ) ) -> I e. LVec )