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 = w ∈ TopMnd ∩ LMod | Scalar ⁡ w ∈ TopRing ∧ ⋅ 𝑠𝑓 ⁡ w ∈ TopOpen ⁡ Scalar ⁡ w × t TopOpen ⁡ w Cn TopOpen ⁡ w

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctlm class TopMod
1 vw setvar w
2 ctmd class TopMnd
3 clmod class LMod
4 2 3 cin class TopMnd ∩ LMod
5 csca class Scalar
6 1 cv setvar w
7 6 5 cfv class Scalar ⁡ w
8 ctrg class TopRing
9 7 8 wcel wff Scalar ⁡ w ∈ TopRing
10 cscaf class ⋅ 𝑠𝑓
11 6 10 cfv class ⋅ 𝑠𝑓 ⁡ w
12 ctopn class TopOpen
13 7 12 cfv class TopOpen ⁡ Scalar ⁡ w
14 ctx class × t
15 6 12 cfv class TopOpen ⁡ w
16 13 15 14 co class TopOpen ⁡ Scalar ⁡ w × t TopOpen ⁡ w
17 ccn class Cn
18 16 15 17 co class TopOpen ⁡ Scalar ⁡ w × t TopOpen ⁡ w Cn TopOpen ⁡ w
19 11 18 wcel wff ⋅ 𝑠𝑓 ⁡ w ∈ TopOpen ⁡ Scalar ⁡ w × t TopOpen ⁡ w Cn TopOpen ⁡ w
20 9 19 wa wff Scalar ⁡ w ∈ TopRing ∧ ⋅ 𝑠𝑓 ⁡ w ∈ TopOpen ⁡ Scalar ⁡ w × t TopOpen ⁡ w Cn TopOpen ⁡ w
21 20 1 4 crab class w ∈ TopMnd ∩ LMod | Scalar ⁡ w ∈ TopRing ∧ ⋅ 𝑠𝑓 ⁡ w ∈ TopOpen ⁡ Scalar ⁡ w × t TopOpen ⁡ w Cn TopOpen ⁡ w
22 0 21 wceq wff TopMod = w ∈ TopMnd ∩ LMod | Scalar ⁡ w ∈ TopRing ∧ ⋅ 𝑠𝑓 ⁡ w ∈ TopOpen ⁡ Scalar ⁡ w × t TopOpen ⁡ w Cn TopOpen ⁡ w