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=\mathrm{Scalar}\left(W\right)$$
Assertion	tvctdrg	$$⊢W\in \mathrm{TopVec}\to F\in \mathrm{TopDRing}$$

Proof

Step	Hyp	Ref	Expression
1		tlmtrg.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
2	1	istvc	$$⊢W\in \mathrm{TopVec}\leftrightarrow \left(W\in \mathrm{TopMod}\wedge F\in \mathrm{TopDRing}\right)$$
3	2	simprbi	$$⊢W\in \mathrm{TopVec}\to F\in \mathrm{TopDRing}$$