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	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
Assertion	istvc	⊢ ( 𝑊 ∈ TopVec ↔ ( 𝑊 ∈ TopMod ∧ 𝐹 ∈ TopDRing ) )

Proof

Step	Hyp	Ref	Expression
1		tlmtrg.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2		fveq2	⊢ ( 𝑥 = 𝑊 → ( Scalar ‘ 𝑥 ) = ( Scalar ‘ 𝑊 ) )
3	2 1	eqtr4di	⊢ ( 𝑥 = 𝑊 → ( Scalar ‘ 𝑥 ) = 𝐹 )
4	3	eleq1d	⊢ ( 𝑥 = 𝑊 → ( ( Scalar ‘ 𝑥 ) ∈ TopDRing ↔ 𝐹 ∈ TopDRing ) )
5		df-tvc	⊢ TopVec = { 𝑥 ∈ TopMod ∣ ( Scalar ‘ 𝑥 ) ∈ TopDRing }
6	4 5	elrab2	⊢ ( 𝑊 ∈ TopVec ↔ ( 𝑊 ∈ TopMod ∧ 𝐹 ∈ TopDRing ) )