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 \in LVec \land F \in (V LMHom U)) \to U \in LVec$

Step	Hyp	Ref	Expression
1		lmhmlmod2	$⊢ F \in (V LMHom U) \to U \in LMod$
2	1	adantl	$⊢ (V \in LVec \land F \in (V LMHom U)) \to U \in LMod$
3		eqid	$⊢ Scalar (V) = Scalar (V)$
4		eqid	$⊢ Scalar (U) = Scalar (U)$
5	3 4	lmhmsca	$⊢ F \in (V LMHom U) \to Scalar (U) = Scalar (V)$
6	5	adantl	$⊢ (V \in LVec \land F \in (V LMHom U)) \to Scalar (U) = Scalar (V)$
7	3	lvecdrng	$⊢ V \in LVec \to Scalar (V) \in DivRing$
8	7	adantr	$⊢ (V \in LVec \land F \in (V LMHom U)) \to Scalar (V) \in DivRing$
9	6 8	eqeltrd	$⊢ (V \in LVec \land F \in (V LMHom U)) \to Scalar (U) \in DivRing$
10	4	islvec	$⊢ U \in LVec \leftrightarrow (U \in LMod \land Scalar (U) \in DivRing)$
11	2 9 10	sylanbrc	$⊢ (V \in LVec \land F \in (V LMHom U)) \to U \in LVec$

Metamath Proof Explorer