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	⊢ 𝐼 = ( 𝑈 ↾s ran 𝐹 )
Assertion	imlmhm	⊢ ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) → 𝐼 ∈ LVec )

Proof

Step	Hyp	Ref	Expression
1		imlmhm.i	⊢ 𝐼 = ( 𝑈 ↾s ran 𝐹 )
2		lmhmlvec2	⊢ ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) → 𝑈 ∈ LVec )
3		lmhmrnlss	⊢ ( 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) → ran 𝐹 ∈ ( LSubSp ‘ 𝑈 ) )
4	3	adantl	⊢ ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) → ran 𝐹 ∈ ( LSubSp ‘ 𝑈 ) )
5		eqid	⊢ ( LSubSp ‘ 𝑈 ) = ( LSubSp ‘ 𝑈 )
6	1 5	lsslvec	⊢ ( ( 𝑈 ∈ LVec ∧ ran 𝐹 ∈ ( LSubSp ‘ 𝑈 ) ) → 𝐼 ∈ LVec )
7	2 4 6	syl2anc	⊢ ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) → 𝐼 ∈ LVec )