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