This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = Scalar (W)$
	Assertion	istvc	$⊢ W \in TopVec \leftrightarrow (W \in TopMod \land F \in TopDRing)$

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