Metamath Proof Explorer

Theorem lmhmlvec2

Description: A homomorphism of left vector spaces has a left vector space as codomain. (Contributed by Thierry Arnoux, 7-May-2023)

Ref Expression
Assertion lmhmlvec2 ⊢ V ∈ LVec ∧ F ∈ V LMHom U → U ∈ LVec

Proof

Step Hyp Ref Expression
1 lmhmlmod2 ⊢ F ∈ V LMHom U → U ∈ LMod
2 1 adantl ⊢ V ∈ LVec ∧ F ∈ V LMHom U → U ∈ LMod
3 eqid ⊢ Scalar ⁡ V = Scalar ⁡ V
4 eqid ⊢ Scalar ⁡ U = Scalar ⁡ U
5 3 4 lmhmsca ⊢ F ∈ V LMHom U → Scalar ⁡ U = Scalar ⁡ V
6 5 adantl ⊢ V ∈ LVec ∧ F ∈ V LMHom U → Scalar ⁡ U = Scalar ⁡ V
7 3 lvecdrng ⊢ V ∈ LVec → Scalar ⁡ V ∈ DivRing
8 7 adantr ⊢ V ∈ LVec ∧ F ∈ V LMHom U → Scalar ⁡ V ∈ DivRing
9 6 8 eqeltrd ⊢ V ∈ LVec ∧ F ∈ V LMHom U → Scalar ⁡ U ∈ DivRing
10 4 islvec ⊢ U ∈ LVec ↔ U ∈ LMod ∧ Scalar ⁡ U ∈ DivRing
11 2 9 10 sylanbrc ⊢ V ∈ LVec ∧ F ∈ V LMHom U → U ∈ LVec