Theorem tvclvec

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

	Ref	Expression
Assertion	tvclvec	|- ( W e. TopVec -> W e. LVec )

Proof

Step	Hyp	Ref	Expression
1		tvclmod	|- ( W e. TopVec -> W e. LMod )
2		eqid	|- ( Scalar ` W ) = ( Scalar ` W )
3	2	tvctdrg	|- ( W e. TopVec -> ( Scalar ` W ) e. TopDRing )
4		tdrgdrng	|- ( ( Scalar ` W ) e. TopDRing -> ( Scalar ` W ) e. DivRing )
5	3 4	syl	|- ( W e. TopVec -> ( Scalar ` W ) e. DivRing )
6	2	islvec	|- ( W e. LVec <-> ( W e. LMod /\ ( Scalar ` W ) e. DivRing ) )
7	1 5 6	sylanbrc	|- ( W e. TopVec -> W e. LVec )