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 ∈ LVec ∧ F ∈ V LMHom U → I ∈ LVec

Proof

Step Hyp Ref Expression
1 imlmhm.i ⊢ I = U ↾ 𝑠 ran ⁡ F
2 lmhmlvec2 ⊢ V ∈ LVec ∧ F ∈ V LMHom U → U ∈ LVec
3 lmhmrnlss ⊢ F ∈ V LMHom U → ran ⁡ F ∈ LSubSp ⁡ U
4 3 adantl ⊢ V ∈ LVec ∧ F ∈ V LMHom U → ran ⁡ F ∈ LSubSp ⁡ U
5 eqid ⊢ LSubSp ⁡ U = LSubSp ⁡ U
6 1 5 lsslvec ⊢ U ∈ LVec ∧ ran ⁡ F ∈ LSubSp ⁡ U → I ∈ LVec
7 2 4 6 syl2anc ⊢ V ∈ LVec ∧ F ∈ V LMHom U → I ∈ LVec