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