Metamath Proof Explorer

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 ↾_{𝑠} ran F$
	Assertion	imlmhm	$⊢ (V \in LVec \land F \in (V LMHom U)) \to I \in LVec$

Step	Hyp	Ref	Expression
1		imlmhm.i	$⊢ I = U ↾_{𝑠} ran F$
2		lmhmlvec2	$⊢ (V \in LVec \land F \in (V LMHom U)) \to U \in LVec$
3		lmhmrnlss	$⊢ F \in (V LMHom U) \to ran F \in LSubSp (U)$
4	3	adantl	$⊢ (V \in LVec \land F \in (V LMHom U)) \to ran F \in LSubSp (U)$
5		eqid	$⊢ LSubSp (U) = LSubSp (U)$
6	1 5	lsslvec	$⊢ (U \in LVec \land ran F \in LSubSp (U)) \to I \in LVec$
7	2 4 6	syl2anc	$⊢ (V \in LVec \land F \in (V LMHom U)) \to I \in LVec$