This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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