tvclvec

Description: A topological vector space is a vector space. (Contributed by Mario Carneiro, 5-Oct-2015)

		Ref	Expression
	Assertion	tvclvec	$⊢ W \in TopVec \to W \in LVec$

Step	Hyp	Ref	Expression
1		tvclmod	$⊢ W \in TopVec \to W \in LMod$
2		eqid	$⊢ Scalar (W) = Scalar (W)$
3	2	tvctdrg	$⊢ W \in TopVec \to Scalar (W) \in TopDRing$
4		tdrgdrng	$⊢ Scalar (W) \in TopDRing \to Scalar (W) \in DivRing$
5	3 4	syl	$⊢ W \in TopVec \to Scalar (W) \in DivRing$
6	2	islvec	$⊢ W \in LVec \leftrightarrow (W \in LMod \land Scalar (W) \in DivRing)$
7	1 5 6	sylanbrc	$⊢ W \in TopVec \to W \in LVec$

Metamath Proof Explorer