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 e. LVec /\ F e. ( V LMHom U ) ) -> U e. LVec )

Proof

Step Hyp Ref Expression
1 lmhmlmod2 
 |-  ( F e. ( V LMHom U ) -> U e. LMod )
2 1 adantl 
 |-  ( ( V e. LVec /\ F e. ( V LMHom U ) ) -> U e. LMod )
3 eqid 
 |-  ( Scalar ` V ) = ( Scalar ` V )
4 eqid 
 |-  ( Scalar ` U ) = ( Scalar ` U )
5 3 4 lmhmsca 
 |-  ( F e. ( V LMHom U ) -> ( Scalar ` U ) = ( Scalar ` V ) )
6 5 adantl 
 |-  ( ( V e. LVec /\ F e. ( V LMHom U ) ) -> ( Scalar ` U ) = ( Scalar ` V ) )
7 3 lvecdrng 
 |-  ( V e. LVec -> ( Scalar ` V ) e. DivRing )
8 7 adantr 
 |-  ( ( V e. LVec /\ F e. ( V LMHom U ) ) -> ( Scalar ` V ) e. DivRing )
9 6 8 eqeltrd 
 |-  ( ( V e. LVec /\ F e. ( V LMHom U ) ) -> ( Scalar ` U ) e. DivRing )
10 4 islvec 
 |-  ( U e. LVec <-> ( U e. LMod /\ ( Scalar ` U ) e. DivRing ) )
11 2 9 10 sylanbrc 
 |-  ( ( V e. LVec /\ F e. ( V LMHom U ) ) -> U e. LVec )