Theorem istvc

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

	Ref	Expression
Hypothesis	tlmtrg.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
Assertion	istvc	$$⊢W\in \mathrm{TopVec}\leftrightarrow \left(W\in \mathrm{TopMod}\wedge F\in \mathrm{TopDRing}\right)$$

Proof

Step	Hyp	Ref	Expression
1		tlmtrg.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
2		fveq2	$$⊢x=W\to \mathrm{Scalar}\left(x\right)=\mathrm{Scalar}\left(W\right)$$
3	2 1	eqtr4di	$$⊢x=W\to \mathrm{Scalar}\left(x\right)=F$$
4	3	eleq1d	$$⊢x=W\to \left(\mathrm{Scalar}\left(x\right)\in \mathrm{TopDRing}\leftrightarrow F\in \mathrm{TopDRing}\right)$$
5		df-tvc	$$⊢\mathrm{TopVec}=\left\{x\in \mathrm{TopMod}|\mathrm{Scalar}\left(x\right)\in \mathrm{TopDRing}\right\}$$
6	4 5	elrab2	$$⊢W\in \mathrm{TopVec}\leftrightarrow \left(W\in \mathrm{TopMod}\wedge F\in \mathrm{TopDRing}\right)$$