Step |
Hyp |
Ref |
Expression |
0 |
|
ctlm |
⊢ TopMod |
1 |
|
vw |
⊢ 𝑤 |
2 |
|
ctmd |
⊢ TopMnd |
3 |
|
clmod |
⊢ LMod |
4 |
2 3
|
cin |
⊢ ( TopMnd ∩ LMod ) |
5 |
|
csca |
⊢ Scalar |
6 |
1
|
cv |
⊢ 𝑤 |
7 |
6 5
|
cfv |
⊢ ( Scalar ‘ 𝑤 ) |
8 |
|
ctrg |
⊢ TopRing |
9 |
7 8
|
wcel |
⊢ ( Scalar ‘ 𝑤 ) ∈ TopRing |
10 |
|
cscaf |
⊢ ·sf |
11 |
6 10
|
cfv |
⊢ ( ·sf ‘ 𝑤 ) |
12 |
|
ctopn |
⊢ TopOpen |
13 |
7 12
|
cfv |
⊢ ( TopOpen ‘ ( Scalar ‘ 𝑤 ) ) |
14 |
|
ctx |
⊢ ×t |
15 |
6 12
|
cfv |
⊢ ( TopOpen ‘ 𝑤 ) |
16 |
13 15 14
|
co |
⊢ ( ( TopOpen ‘ ( Scalar ‘ 𝑤 ) ) ×t ( TopOpen ‘ 𝑤 ) ) |
17 |
|
ccn |
⊢ Cn |
18 |
16 15 17
|
co |
⊢ ( ( ( TopOpen ‘ ( Scalar ‘ 𝑤 ) ) ×t ( TopOpen ‘ 𝑤 ) ) Cn ( TopOpen ‘ 𝑤 ) ) |
19 |
11 18
|
wcel |
⊢ ( ·sf ‘ 𝑤 ) ∈ ( ( ( TopOpen ‘ ( Scalar ‘ 𝑤 ) ) ×t ( TopOpen ‘ 𝑤 ) ) Cn ( TopOpen ‘ 𝑤 ) ) |
20 |
9 19
|
wa |
⊢ ( ( Scalar ‘ 𝑤 ) ∈ TopRing ∧ ( ·sf ‘ 𝑤 ) ∈ ( ( ( TopOpen ‘ ( Scalar ‘ 𝑤 ) ) ×t ( TopOpen ‘ 𝑤 ) ) Cn ( TopOpen ‘ 𝑤 ) ) ) |
21 |
20 1 4
|
crab |
⊢ { 𝑤 ∈ ( TopMnd ∩ LMod ) ∣ ( ( Scalar ‘ 𝑤 ) ∈ TopRing ∧ ( ·sf ‘ 𝑤 ) ∈ ( ( ( TopOpen ‘ ( Scalar ‘ 𝑤 ) ) ×t ( TopOpen ‘ 𝑤 ) ) Cn ( TopOpen ‘ 𝑤 ) ) ) } |
22 |
0 21
|
wceq |
⊢ TopMod = { 𝑤 ∈ ( TopMnd ∩ LMod ) ∣ ( ( Scalar ‘ 𝑤 ) ∈ TopRing ∧ ( ·sf ‘ 𝑤 ) ∈ ( ( ( TopOpen ‘ ( Scalar ‘ 𝑤 ) ) ×t ( TopOpen ‘ 𝑤 ) ) Cn ( TopOpen ‘ 𝑤 ) ) ) } |