Metamath Proof Explorer


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 ‘ 𝑤 ) ) ) }