Metamath Proof Explorer

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 
|- F = ( Scalar ` W )
Assertion tlmtrg 
|- ( W e. TopMod -> F e. TopRing )

Proof

Step Hyp Ref Expression
1 tlmtrg.f 
 |-  F = ( Scalar ` W )
2 eqid 
 |-  ( .sf ` W ) = ( .sf ` W )
3 eqid 
 |-  ( TopOpen ` W ) = ( TopOpen ` W )
4 eqid 
 |-  ( TopOpen ` F ) = ( TopOpen ` F )
5 2 3 1 4 istlm 
 |-  ( W e. TopMod <-> ( ( W e. TopMnd /\ W e. LMod /\ F e. TopRing ) /\ ( .sf ` W ) e. ( ( ( TopOpen ` F ) tX ( TopOpen ` W ) ) Cn ( TopOpen ` W ) ) ) )
6 5 simplbi 
 |-  ( W e. TopMod -> ( W e. TopMnd /\ W e. LMod /\ F e. TopRing ) )
7 6 simp3d 
 |-  ( W e. TopMod -> F e. TopRing )