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 𝐹 = ( Scalar ‘ 𝑊 )
Assertion tvctdrg ( 𝑊 ∈ TopVec → 𝐹 ∈ TopDRing )

Proof

Step Hyp Ref Expression
1 tlmtrg.f 𝐹 = ( Scalar ‘ 𝑊 )
2 1 istvc ( 𝑊 ∈ TopVec ↔ ( 𝑊 ∈ TopMod ∧ 𝐹 ∈ TopDRing ) )
3 2 simprbi ( 𝑊 ∈ TopVec → 𝐹 ∈ TopDRing )