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=ScalarW
Assertion tvctdrg WTopVecFTopDRing

Proof

Step Hyp Ref Expression
1 tlmtrg.f F=ScalarW
2 1 istvc WTopVecWTopModFTopDRing
3 2 simprbi WTopVecFTopDRing