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×tTopOpen⁡wCnTopOpen⁡w

Detailed syntax breakdown

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