Theorem tlmtrg

Description: The scalar ring of a topological module is a topological ring. (Contributed by Mario Carneiro, 5-Oct-2015)

	Ref	Expression
Hypothesis	tlmtrg.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
Assertion	tlmtrg	⊢ ( 𝑊 ∈ TopMod → 𝐹 ∈ TopRing )

Proof

Step	Hyp	Ref	Expression
1		tlmtrg.f	⊢ 𝐹 = ( Scalar ‘ 𝑊 )
2		eqid	⊢ ( ·sf ‘ 𝑊 ) = ( ·sf ‘ 𝑊 )
3		eqid	⊢ ( TopOpen ‘ 𝑊 ) = ( TopOpen ‘ 𝑊 )
4		eqid	⊢ ( TopOpen ‘ 𝐹 ) = ( TopOpen ‘ 𝐹 )
5	2 3 1 4	istlm	⊢ ( 𝑊 ∈ TopMod ↔ ( ( 𝑊 ∈ TopMnd ∧ 𝑊 ∈ LMod ∧ 𝐹 ∈ TopRing ) ∧ ( ·sf ‘ 𝑊 ) ∈ ( ( ( TopOpen ‘ 𝐹 ) ×t ( TopOpen ‘ 𝑊 ) ) Cn ( TopOpen ‘ 𝑊 ) ) ) )
6	5	simplbi	⊢ ( 𝑊 ∈ TopMod → ( 𝑊 ∈ TopMnd ∧ 𝑊 ∈ LMod ∧ 𝐹 ∈ TopRing ) )
7	6	simp3d	⊢ ( 𝑊 ∈ TopMod → 𝐹 ∈ TopRing )