Theorem tvclvec

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

	Ref	Expression
Assertion	tvclvec	⊢ ( 𝑊 ∈ TopVec → 𝑊 ∈ LVec )

Proof

Step	Hyp	Ref	Expression
1		tvclmod	⊢ ( 𝑊 ∈ TopVec → 𝑊 ∈ LMod )
2		eqid	⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
3	2	tvctdrg	⊢ ( 𝑊 ∈ TopVec → ( Scalar ‘ 𝑊 ) ∈ TopDRing )
4		tdrgdrng	⊢ ( ( Scalar ‘ 𝑊 ) ∈ TopDRing → ( Scalar ‘ 𝑊 ) ∈ DivRing )
5	3 4	syl	⊢ ( 𝑊 ∈ TopVec → ( Scalar ‘ 𝑊 ) ∈ DivRing )
6	2	islvec	⊢ ( 𝑊 ∈ LVec ↔ ( 𝑊 ∈ LMod ∧ ( Scalar ‘ 𝑊 ) ∈ DivRing ) )
7	1 5 6	sylanbrc	⊢ ( 𝑊 ∈ TopVec → 𝑊 ∈ LVec )