Description: Define a topological left vector space, which is a topological module over a topological division ring. (Contributed by Mario Carneiro, 5-Oct-2015)
Ref | Expression | ||
---|---|---|---|
Assertion | df-tvc | |
Step | Hyp | Ref | Expression |
---|---|---|---|
0 | ctvc | |
|
1 | vw | |
|
2 | ctlm | |
|
3 | csca | |
|
4 | 1 | cv | |
5 | 4 3 | cfv | |
6 | ctdrg | |
|
7 | 5 6 | wcel | |
8 | 7 1 2 | crab | |
9 | 0 8 | wceq | |