Step |
Hyp |
Ref |
Expression |
1 |
|
smcn.c |
⊢ 𝐶 = ( IndMet ‘ 𝑈 ) |
2 |
|
smcn.j |
⊢ 𝐽 = ( MetOpen ‘ 𝐶 ) |
3 |
|
smcn.s |
⊢ 𝑆 = ( ·𝑠OLD ‘ 𝑈 ) |
4 |
|
smcn.k |
⊢ 𝐾 = ( TopOpen ‘ ℂfld ) |
5 |
|
fveq2 |
⊢ ( 𝑈 = if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) → ( ·𝑠OLD ‘ 𝑈 ) = ( ·𝑠OLD ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) ) |
6 |
3 5
|
syl5eq |
⊢ ( 𝑈 = if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) → 𝑆 = ( ·𝑠OLD ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) ) |
7 |
|
fveq2 |
⊢ ( 𝑈 = if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) → ( IndMet ‘ 𝑈 ) = ( IndMet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) ) |
8 |
1 7
|
syl5eq |
⊢ ( 𝑈 = if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) → 𝐶 = ( IndMet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) ) |
9 |
8
|
fveq2d |
⊢ ( 𝑈 = if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) → ( MetOpen ‘ 𝐶 ) = ( MetOpen ‘ ( IndMet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) ) ) |
10 |
2 9
|
syl5eq |
⊢ ( 𝑈 = if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) → 𝐽 = ( MetOpen ‘ ( IndMet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) ) ) |
11 |
10
|
oveq2d |
⊢ ( 𝑈 = if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) → ( 𝐾 ×t 𝐽 ) = ( 𝐾 ×t ( MetOpen ‘ ( IndMet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) ) ) ) |
12 |
11 10
|
oveq12d |
⊢ ( 𝑈 = if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) → ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) = ( ( 𝐾 ×t ( MetOpen ‘ ( IndMet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) ) ) Cn ( MetOpen ‘ ( IndMet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) ) ) ) |
13 |
6 12
|
eleq12d |
⊢ ( 𝑈 = if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) → ( 𝑆 ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) ↔ ( ·𝑠OLD ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) ∈ ( ( 𝐾 ×t ( MetOpen ‘ ( IndMet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) ) ) Cn ( MetOpen ‘ ( IndMet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) ) ) ) ) |
14 |
|
eqid |
⊢ ( IndMet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) = ( IndMet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) |
15 |
|
eqid |
⊢ ( MetOpen ‘ ( IndMet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) ) = ( MetOpen ‘ ( IndMet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) ) |
16 |
|
eqid |
⊢ ( ·𝑠OLD ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) = ( ·𝑠OLD ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) |
17 |
|
eqid |
⊢ ( BaseSet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) = ( BaseSet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) |
18 |
|
eqid |
⊢ ( normCV ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) = ( normCV ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) |
19 |
|
elimnvu |
⊢ if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ∈ NrmCVec |
20 |
|
eqid |
⊢ ( 1 / ( 1 + ( ( ( ( ( normCV ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) ) = ( 1 / ( 1 + ( ( ( ( ( normCV ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) ‘ 𝑦 ) + ( abs ‘ 𝑥 ) ) + 1 ) / 𝑟 ) ) ) |
21 |
14 15 16 4 17 18 19 20
|
smcnlem |
⊢ ( ·𝑠OLD ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) ∈ ( ( 𝐾 ×t ( MetOpen ‘ ( IndMet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) ) ) Cn ( MetOpen ‘ ( IndMet ‘ if ( 𝑈 ∈ NrmCVec , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) ) ) |
22 |
13 21
|
dedth |
⊢ ( 𝑈 ∈ NrmCVec → 𝑆 ∈ ( ( 𝐾 ×t 𝐽 ) Cn 𝐽 ) ) |