Step |
Hyp |
Ref |
Expression |
1 |
|
ubth.1 |
⊢ 𝑋 = ( BaseSet ‘ 𝑈 ) |
2 |
|
ubth.2 |
⊢ 𝑁 = ( normCV ‘ 𝑊 ) |
3 |
|
ubth.3 |
⊢ 𝑀 = ( 𝑈 normOpOLD 𝑊 ) |
4 |
|
oveq1 |
⊢ ( 𝑈 = if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) → ( 𝑈 BLnOp 𝑊 ) = ( if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) BLnOp 𝑊 ) ) |
5 |
4
|
sseq2d |
⊢ ( 𝑈 = if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) → ( 𝑇 ⊆ ( 𝑈 BLnOp 𝑊 ) ↔ 𝑇 ⊆ ( if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) BLnOp 𝑊 ) ) ) |
6 |
|
fveq2 |
⊢ ( 𝑈 = if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) → ( BaseSet ‘ 𝑈 ) = ( BaseSet ‘ if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) ) |
7 |
1 6
|
syl5eq |
⊢ ( 𝑈 = if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) → 𝑋 = ( BaseSet ‘ if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) ) |
8 |
7
|
raleqdv |
⊢ ( 𝑈 = if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) → ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ↔ ∀ 𝑥 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ) ) |
9 |
|
oveq1 |
⊢ ( 𝑈 = if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) → ( 𝑈 normOpOLD 𝑊 ) = ( if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) normOpOLD 𝑊 ) ) |
10 |
3 9
|
syl5eq |
⊢ ( 𝑈 = if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) → 𝑀 = ( if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) normOpOLD 𝑊 ) ) |
11 |
10
|
fveq1d |
⊢ ( 𝑈 = if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) → ( 𝑀 ‘ 𝑡 ) = ( ( if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) normOpOLD 𝑊 ) ‘ 𝑡 ) ) |
12 |
11
|
breq1d |
⊢ ( 𝑈 = if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) → ( ( 𝑀 ‘ 𝑡 ) ≤ 𝑑 ↔ ( ( if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) |
13 |
12
|
rexralbidv |
⊢ ( 𝑈 = if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) → ( ∃ 𝑑 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑀 ‘ 𝑡 ) ≤ 𝑑 ↔ ∃ 𝑑 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( ( if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) |
14 |
8 13
|
bibi12d |
⊢ ( 𝑈 = if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) → ( ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ↔ ∃ 𝑑 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑀 ‘ 𝑡 ) ≤ 𝑑 ) ↔ ( ∀ 𝑥 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ↔ ∃ 𝑑 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( ( if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) ) |
15 |
5 14
|
imbi12d |
⊢ ( 𝑈 = if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) → ( ( 𝑇 ⊆ ( 𝑈 BLnOp 𝑊 ) → ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ↔ ∃ 𝑑 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑀 ‘ 𝑡 ) ≤ 𝑑 ) ) ↔ ( 𝑇 ⊆ ( if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) BLnOp 𝑊 ) → ( ∀ 𝑥 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ↔ ∃ 𝑑 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( ( if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) ) ) |
16 |
|
oveq2 |
⊢ ( 𝑊 = if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) → ( if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) BLnOp 𝑊 ) = ( if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) BLnOp if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) ) ) |
17 |
16
|
sseq2d |
⊢ ( 𝑊 = if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) → ( 𝑇 ⊆ ( if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) BLnOp 𝑊 ) ↔ 𝑇 ⊆ ( if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) BLnOp if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) ) ) ) |
18 |
|
fveq2 |
⊢ ( 𝑊 = if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) → ( normCV ‘ 𝑊 ) = ( normCV ‘ if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) ) ) |
19 |
2 18
|
syl5eq |
⊢ ( 𝑊 = if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) → 𝑁 = ( normCV ‘ if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) ) ) |
20 |
19
|
fveq1d |
⊢ ( 𝑊 = if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) → ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) = ( ( normCV ‘ if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) ) ‘ ( 𝑡 ‘ 𝑥 ) ) ) |
21 |
20
|
breq1d |
⊢ ( 𝑊 = if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) → ( ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ↔ ( ( normCV ‘ if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) ) ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ) ) |
22 |
21
|
rexralbidv |
⊢ ( 𝑊 = if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) → ( ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ↔ ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( ( normCV ‘ if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) ) ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ) ) |
23 |
22
|
ralbidv |
⊢ ( 𝑊 = if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) → ( ∀ 𝑥 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ↔ ∀ 𝑥 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( ( normCV ‘ if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) ) ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ) ) |
24 |
|
oveq2 |
⊢ ( 𝑊 = if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) → ( if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) normOpOLD 𝑊 ) = ( if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) normOpOLD if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) ) ) |
25 |
24
|
fveq1d |
⊢ ( 𝑊 = if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) → ( ( if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) normOpOLD 𝑊 ) ‘ 𝑡 ) = ( ( if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) normOpOLD if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) ) ‘ 𝑡 ) ) |
26 |
25
|
breq1d |
⊢ ( 𝑊 = if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) → ( ( ( if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ↔ ( ( if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) normOpOLD if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) ) ‘ 𝑡 ) ≤ 𝑑 ) ) |
27 |
26
|
rexralbidv |
⊢ ( 𝑊 = if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) → ( ∃ 𝑑 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( ( if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ↔ ∃ 𝑑 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( ( if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) normOpOLD if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) ) ‘ 𝑡 ) ≤ 𝑑 ) ) |
28 |
23 27
|
bibi12d |
⊢ ( 𝑊 = if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) → ( ( ∀ 𝑥 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ↔ ∃ 𝑑 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( ( if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ↔ ( ∀ 𝑥 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( ( normCV ‘ if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) ) ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ↔ ∃ 𝑑 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( ( if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) normOpOLD if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) ) ‘ 𝑡 ) ≤ 𝑑 ) ) ) |
29 |
17 28
|
imbi12d |
⊢ ( 𝑊 = if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) → ( ( 𝑇 ⊆ ( if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) BLnOp 𝑊 ) → ( ∀ 𝑥 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ↔ ∃ 𝑑 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( ( if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) normOpOLD 𝑊 ) ‘ 𝑡 ) ≤ 𝑑 ) ) ↔ ( 𝑇 ⊆ ( if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) BLnOp if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) ) → ( ∀ 𝑥 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( ( normCV ‘ if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) ) ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ↔ ∃ 𝑑 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( ( if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) normOpOLD if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) ) ‘ 𝑡 ) ≤ 𝑑 ) ) ) ) |
30 |
|
eqid |
⊢ ( BaseSet ‘ if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) = ( BaseSet ‘ if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) |
31 |
|
eqid |
⊢ ( normCV ‘ if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) ) = ( normCV ‘ if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) ) |
32 |
|
eqid |
⊢ ( IndMet ‘ if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) = ( IndMet ‘ if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) |
33 |
|
eqid |
⊢ ( MetOpen ‘ ( IndMet ‘ if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) ) = ( MetOpen ‘ ( IndMet ‘ if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) ) |
34 |
|
eqid |
⊢ 〈 〈 + , · 〉 , abs 〉 = 〈 〈 + , · 〉 , abs 〉 |
35 |
34
|
cnbn |
⊢ 〈 〈 + , · 〉 , abs 〉 ∈ CBan |
36 |
35
|
elimel |
⊢ if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ∈ CBan |
37 |
|
elimnvu |
⊢ if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) ∈ NrmCVec |
38 |
|
id |
⊢ ( 𝑇 ⊆ ( if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) BLnOp if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) ) → 𝑇 ⊆ ( if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) BLnOp if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) ) ) |
39 |
30 31 32 33 36 37 38
|
ubthlem3 |
⊢ ( 𝑇 ⊆ ( if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) BLnOp if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) ) → ( ∀ 𝑥 ∈ ( BaseSet ‘ if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) ) ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( ( normCV ‘ if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) ) ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ↔ ∃ 𝑑 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( ( if ( 𝑈 ∈ CBan , 𝑈 , 〈 〈 + , · 〉 , abs 〉 ) normOpOLD if ( 𝑊 ∈ NrmCVec , 𝑊 , 〈 〈 + , · 〉 , abs 〉 ) ) ‘ 𝑡 ) ≤ 𝑑 ) ) |
40 |
15 29 39
|
dedth2h |
⊢ ( ( 𝑈 ∈ CBan ∧ 𝑊 ∈ NrmCVec ) → ( 𝑇 ⊆ ( 𝑈 BLnOp 𝑊 ) → ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ↔ ∃ 𝑑 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑀 ‘ 𝑡 ) ≤ 𝑑 ) ) ) |
41 |
40
|
3impia |
⊢ ( ( 𝑈 ∈ CBan ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ⊆ ( 𝑈 BLnOp 𝑊 ) ) → ( ∀ 𝑥 ∈ 𝑋 ∃ 𝑐 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑁 ‘ ( 𝑡 ‘ 𝑥 ) ) ≤ 𝑐 ↔ ∃ 𝑑 ∈ ℝ ∀ 𝑡 ∈ 𝑇 ( 𝑀 ‘ 𝑡 ) ≤ 𝑑 ) ) |