Definition df-tlm

Description: Define a topological left module, which is just what its name suggests: instead of a group over a ring with a scalar product connecting them, it is a topological group over a topological ring with a continuous scalar product. (Contributed by Mario Carneiro, 5-Oct-2015)

	Ref	Expression
Assertion	df-tlm	⊢ TopMod = { 𝑤 ∈ ( TopMnd ∩ LMod ) ∣ ( ( Scalar ‘ 𝑤 ) ∈ TopRing ∧ ( ·sf ‘ 𝑤 ) ∈ ( ( ( TopOpen ‘ ( Scalar ‘ 𝑤 ) ) ×t ( TopOpen ‘ 𝑤 ) ) Cn ( TopOpen ‘ 𝑤 ) ) ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ctlm	⊢ TopMod
1		vw	⊢ 𝑤
2		ctmd	⊢ TopMnd
3		clmod	⊢ LMod
4	2 3	cin	⊢ ( TopMnd ∩ LMod )
5		csca	⊢ Scalar
6	1	cv	⊢ 𝑤
7	6 5	cfv	⊢ ( Scalar ‘ 𝑤 )
8		ctrg	⊢ TopRing
9	7 8	wcel	⊢ ( Scalar ‘ 𝑤 ) ∈ TopRing
10		cscaf	⊢ ·sf
11	6 10	cfv	⊢ ( ·sf ‘ 𝑤 )
12		ctopn	⊢ TopOpen
13	7 12	cfv	⊢ ( TopOpen ‘ ( Scalar ‘ 𝑤 ) )
14		ctx	⊢ ×t
15	6 12	cfv	⊢ ( TopOpen ‘ 𝑤 )
16	13 15 14	co	⊢ ( ( TopOpen ‘ ( Scalar ‘ 𝑤 ) ) ×t ( TopOpen ‘ 𝑤 ) )
17		ccn	⊢ Cn
18	16 15 17	co	⊢ ( ( ( TopOpen ‘ ( Scalar ‘ 𝑤 ) ) ×t ( TopOpen ‘ 𝑤 ) ) Cn ( TopOpen ‘ 𝑤 ) )
19	11 18	wcel	⊢ ( ·sf ‘ 𝑤 ) ∈ ( ( ( TopOpen ‘ ( Scalar ‘ 𝑤 ) ) ×t ( TopOpen ‘ 𝑤 ) ) Cn ( TopOpen ‘ 𝑤 ) )
20	9 19	wa	⊢ ( ( Scalar ‘ 𝑤 ) ∈ TopRing ∧ ( ·sf ‘ 𝑤 ) ∈ ( ( ( TopOpen ‘ ( Scalar ‘ 𝑤 ) ) ×t ( TopOpen ‘ 𝑤 ) ) Cn ( TopOpen ‘ 𝑤 ) ) )
21	20 1 4	crab	⊢ { 𝑤 ∈ ( TopMnd ∩ LMod ) ∣ ( ( Scalar ‘ 𝑤 ) ∈ TopRing ∧ ( ·sf ‘ 𝑤 ) ∈ ( ( ( TopOpen ‘ ( Scalar ‘ 𝑤 ) ) ×t ( TopOpen ‘ 𝑤 ) ) Cn ( TopOpen ‘ 𝑤 ) ) ) }
22	0 21	wceq	⊢ TopMod = { 𝑤 ∈ ( TopMnd ∩ LMod ) ∣ ( ( Scalar ‘ 𝑤 ) ∈ TopRing ∧ ( ·sf ‘ 𝑤 ) ∈ ( ( ( TopOpen ‘ ( Scalar ‘ 𝑤 ) ) ×t ( TopOpen ‘ 𝑤 ) ) Cn ( TopOpen ‘ 𝑤 ) ) ) }