Metamath Proof Explorer


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 )