Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-tlm Structured version   Unicode version

Definition df-tlm 18196
 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.)
Assertion
Ref Expression
df-tlm TopMod TopMnd Scalar Scalar

Detailed syntax breakdown of Definition df-tlm
StepHypRef Expression
1 ctlm 18192 . 2 TopMod
2 vw . . . . . . 7
32cv 1652 . . . . . 6
4 csca 13537 . . . . . 6 Scalar
53, 4cfv 5457 . . . . 5 Scalar
6 ctrg 18190 . . . . 5
75, 6wcel 1726 . . . 4 Scalar
8 cscaf 15956 . . . . . 6
93, 8cfv 5457 . . . . 5
10 ctopn 13654 . . . . . . . 8
115, 10cfv 5457 . . . . . . 7 Scalar
123, 10cfv 5457 . . . . . . 7
13 ctx 17597 . . . . . . 7
1411, 12, 13co 6084 . . . . . 6 Scalar
15 ccn 17293 . . . . . 6
1614, 12, 15co 6084 . . . . 5 Scalar
179, 16wcel 1726 . . . 4 Scalar
187, 17wa 360 . . 3 Scalar Scalar
19 ctmd 18105 . . . 4 TopMnd
20 clmod 15955 . . . 4
2119, 20cin 3321 . . 3 TopMnd
2218, 2, 21crab 2711 . 2 TopMnd Scalar Scalar
231, 22wceq 1653 1 TopMod TopMnd Scalar Scalar
 Colors of variables: wff set class This definition is referenced by:  istlm  18219
 Copyright terms: Public domain W3C validator