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 e. ( TopMnd i^i LMod ) | ( ( Scalar ` w ) e. TopRing /\ ( .sf ` w ) e. ( ( ( TopOpen ` ( Scalar ` w ) ) tX ( TopOpen ` w ) ) Cn ( TopOpen ` w ) ) ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ctlm
 |-  TopMod
1 vw
 |-  w
2 ctmd
 |-  TopMnd
3 clmod
 |-  LMod
4 2 3 cin
 |-  ( TopMnd i^i LMod )
5 csca
 |-  Scalar
6 1 cv
 |-  w
7 6 5 cfv
 |-  ( Scalar ` w )
8 ctrg
 |-  TopRing
9 7 8 wcel
 |-  ( Scalar ` w ) e. TopRing
10 cscaf
 |-  .sf
11 6 10 cfv
 |-  ( .sf ` w )
12 ctopn
 |-  TopOpen
13 7 12 cfv
 |-  ( TopOpen ` ( Scalar ` w ) )
14 ctx
 |-  tX
15 6 12 cfv
 |-  ( TopOpen ` w )
16 13 15 14 co
 |-  ( ( TopOpen ` ( Scalar ` w ) ) tX ( TopOpen ` w ) )
17 ccn
 |-  Cn
18 16 15 17 co
 |-  ( ( ( TopOpen ` ( Scalar ` w ) ) tX ( TopOpen ` w ) ) Cn ( TopOpen ` w ) )
19 11 18 wcel
 |-  ( .sf ` w ) e. ( ( ( TopOpen ` ( Scalar ` w ) ) tX ( TopOpen ` w ) ) Cn ( TopOpen ` w ) )
20 9 19 wa
 |-  ( ( Scalar ` w ) e. TopRing /\ ( .sf ` w ) e. ( ( ( TopOpen ` ( Scalar ` w ) ) tX ( TopOpen ` w ) ) Cn ( TopOpen ` w ) ) )
21 20 1 4 crab
 |-  { w e. ( TopMnd i^i LMod ) | ( ( Scalar ` w ) e. TopRing /\ ( .sf ` w ) e. ( ( ( TopOpen ` ( Scalar ` w ) ) tX ( TopOpen ` w ) ) Cn ( TopOpen ` w ) ) ) }
22 0 21 wceq
 |-  TopMod = { w e. ( TopMnd i^i LMod ) | ( ( Scalar ` w ) e. TopRing /\ ( .sf ` w ) e. ( ( ( TopOpen ` ( Scalar ` w ) ) tX ( TopOpen ` w ) ) Cn ( TopOpen ` w ) ) ) }