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 ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) → 𝑈 ∈ LVec )

Proof

Step Hyp Ref Expression
1 lmhmlmod2 ⊢ ( 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) → 𝑈 ∈ LMod )
2 1 adantl ⊢ ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) → 𝑈 ∈ LMod )
3 eqid ⊢ ( Scalar ‘ 𝑉 ) = ( Scalar ‘ 𝑉 )
4 eqid ⊢ ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑈 )
5 3 4 lmhmsca ⊢ ( 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) → ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑉 ) )
6 5 adantl ⊢ ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) → ( Scalar ‘ 𝑈 ) = ( Scalar ‘ 𝑉 ) )
7 3 lvecdrng ⊢ ( 𝑉 ∈ LVec → ( Scalar ‘ 𝑉 ) ∈ DivRing )
8 7 adantr ⊢ ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) → ( Scalar ‘ 𝑉 ) ∈ DivRing )
9 6 8 eqeltrd ⊢ ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) → ( Scalar ‘ 𝑈 ) ∈ DivRing )
10 4 islvec ⊢ ( 𝑈 ∈ LVec ↔ ( 𝑈 ∈ LMod ∧ ( Scalar ‘ 𝑈 ) ∈ DivRing ) )
11 2 9 10 sylanbrc ⊢ ( ( 𝑉 ∈ LVec ∧ 𝐹 ∈ ( 𝑉 LMHom 𝑈 ) ) → 𝑈 ∈ LVec )