Theorem tvctdrg

Description: The scalar field of a topological vector space is a topological division ring. (Contributed by Mario Carneiro, 5-Oct-2015)

	Ref	Expression
Hypothesis	tlmtrg.f	|- F = ( Scalar ` W )
Assertion	tvctdrg	|- ( W e. TopVec -> F e. TopDRing )

Proof

Step	Hyp	Ref	Expression
1		tlmtrg.f	|- F = ( Scalar ` W )
2	1	istvc	|- ( W e. TopVec <-> ( W e. TopMod /\ F e. TopDRing ) )
3	2	simprbi	|- ( W e. TopVec -> F e. TopDRing )