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=\mathrm{Scalar}\left(W\right)$$
Assertion	tlmtrg	$$⊢W\in \mathrm{TopMod}\to F\in \mathrm{TopRing}$$

Proof

Step	Hyp	Ref	Expression
1		tlmtrg.f	$$⊢F=\mathrm{Scalar}\left(W\right)$$
2		eqid	$$⊢{\cdot }_{\mathrm{𝑠𝑓}}\left(W\right)={\cdot }_{\mathrm{𝑠𝑓}}\left(W\right)$$
3		eqid	$$⊢\mathrm{TopOpen}\left(W\right)=\mathrm{TopOpen}\left(W\right)$$
4		eqid	$$⊢\mathrm{TopOpen}\left(F\right)=\mathrm{TopOpen}\left(F\right)$$
5	2 3 1 4	istlm	$$⊢W\in \mathrm{TopMod}\leftrightarrow \left(\left(W\in \mathrm{TopMnd}\wedge W\in \mathrm{LMod}\wedge F\in \mathrm{TopRing}\right)\wedge {\cdot }_{\mathrm{𝑠𝑓}}\left(W\right)\in \left(\left(\mathrm{TopOpen}\left(F\right){\times }_t\mathrm{TopOpen}\left(W\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left(W\right)\right)\right)$$
6	5	simplbi	$$⊢W\in \mathrm{TopMod}\to \left(W\in \mathrm{TopMnd}\wedge W\in \mathrm{LMod}\wedge F\in \mathrm{TopRing}\right)$$
7	6	simp3d	$$⊢W\in \mathrm{TopMod}\to F\in \mathrm{TopRing}$$