Proof of Theorem ubth
Step | Hyp | Ref
| Expression |
1 | | oveq1 7274 |
. . . . 5
⊢ (𝑈 = if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) → (𝑈 BLnOp
𝑊) = (if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) BLnOp 𝑊)) |
2 | 1 | sseq2d 3952 |
. . . 4
⊢ (𝑈 = if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) → (𝑇
⊆ (𝑈 BLnOp 𝑊) ↔ 𝑇 ⊆ (if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) BLnOp 𝑊))) |
3 | | ubth.1 |
. . . . . . 7
⊢ 𝑋 = (BaseSet‘𝑈) |
4 | | fveq2 6766 |
. . . . . . 7
⊢ (𝑈 = if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) → (BaseSet‘𝑈) = (BaseSet‘if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉))) |
5 | 3, 4 | eqtrid 2790 |
. . . . . 6
⊢ (𝑈 = if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) → 𝑋 =
(BaseSet‘if(𝑈 ∈
CBan, 𝑈, 〈〈 + ,
· 〉, abs〉))) |
6 | 5 | raleqdv 3346 |
. . . . 5
⊢ (𝑈 = if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) → (∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ↔ ∀𝑥 ∈ (BaseSet‘if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉))∃𝑐 ∈
ℝ ∀𝑡 ∈
𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐)) |
7 | | ubth.3 |
. . . . . . . . 9
⊢ 𝑀 = (𝑈 normOpOLD 𝑊) |
8 | | oveq1 7274 |
. . . . . . . . 9
⊢ (𝑈 = if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) → (𝑈
normOpOLD 𝑊) =
(if(𝑈 ∈ CBan, 𝑈, 〈〈 + , ·
〉, abs〉) normOpOLD 𝑊)) |
9 | 7, 8 | eqtrid 2790 |
. . . . . . . 8
⊢ (𝑈 = if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) → 𝑀 =
(if(𝑈 ∈ CBan, 𝑈, 〈〈 + , ·
〉, abs〉) normOpOLD 𝑊)) |
10 | 9 | fveq1d 6768 |
. . . . . . 7
⊢ (𝑈 = if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) → (𝑀‘𝑡) = ((if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) normOpOLD 𝑊)‘𝑡)) |
11 | 10 | breq1d 5083 |
. . . . . 6
⊢ (𝑈 = if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) → ((𝑀‘𝑡) ≤ 𝑑 ↔ ((if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) normOpOLD 𝑊)‘𝑡) ≤ 𝑑)) |
12 | 11 | rexralbidv 3228 |
. . . . 5
⊢ (𝑈 = if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) → (∃𝑑
∈ ℝ ∀𝑡
∈ 𝑇 (𝑀‘𝑡) ≤ 𝑑 ↔ ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 ((if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) normOpOLD 𝑊)‘𝑡) ≤ 𝑑)) |
13 | 6, 12 | bibi12d 346 |
. . . 4
⊢ (𝑈 = if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) → ((∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ↔ ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑀‘𝑡) ≤ 𝑑) ↔ (∀𝑥 ∈ (BaseSet‘if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉))∃𝑐 ∈
ℝ ∀𝑡 ∈
𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ↔ ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 ((if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) normOpOLD 𝑊)‘𝑡) ≤ 𝑑))) |
14 | 2, 13 | imbi12d 345 |
. . 3
⊢ (𝑈 = if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) → ((𝑇
⊆ (𝑈 BLnOp 𝑊) → (∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ↔ ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑀‘𝑡) ≤ 𝑑)) ↔ (𝑇 ⊆ (if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) BLnOp 𝑊) →
(∀𝑥 ∈
(BaseSet‘if(𝑈 ∈
CBan, 𝑈, 〈〈 + ,
· 〉, abs〉))∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ↔ ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 ((if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) normOpOLD 𝑊)‘𝑡) ≤ 𝑑)))) |
15 | | oveq2 7275 |
. . . . 5
⊢ (𝑊 = if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉) → (if(𝑈
∈ CBan, 𝑈,
〈〈 + , · 〉, abs〉) BLnOp 𝑊) = (if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) BLnOp if(𝑊
∈ NrmCVec, 𝑊,
〈〈 + , · 〉, abs〉))) |
16 | 15 | sseq2d 3952 |
. . . 4
⊢ (𝑊 = if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉) → (𝑇
⊆ (if(𝑈 ∈ CBan,
𝑈, 〈〈 + ,
· 〉, abs〉) BLnOp 𝑊) ↔ 𝑇 ⊆ (if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) BLnOp if(𝑊
∈ NrmCVec, 𝑊,
〈〈 + , · 〉, abs〉)))) |
17 | | ubth.2 |
. . . . . . . . . 10
⊢ 𝑁 =
(normCV‘𝑊) |
18 | | fveq2 6766 |
. . . . . . . . . 10
⊢ (𝑊 = if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉) → (normCV‘𝑊) = (normCV‘if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , ·
〉, abs〉))) |
19 | 17, 18 | eqtrid 2790 |
. . . . . . . . 9
⊢ (𝑊 = if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉) → 𝑁 =
(normCV‘if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉))) |
20 | 19 | fveq1d 6768 |
. . . . . . . 8
⊢ (𝑊 = if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉) → (𝑁‘(𝑡‘𝑥)) = ((normCV‘if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , ·
〉, abs〉))‘(𝑡‘𝑥))) |
21 | 20 | breq1d 5083 |
. . . . . . 7
⊢ (𝑊 = if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉) → ((𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ↔ ((normCV‘if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , ·
〉, abs〉))‘(𝑡‘𝑥)) ≤ 𝑐)) |
22 | 21 | rexralbidv 3228 |
. . . . . 6
⊢ (𝑊 = if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉) → (∃𝑐
∈ ℝ ∀𝑡
∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ↔ ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 ((normCV‘if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , ·
〉, abs〉))‘(𝑡‘𝑥)) ≤ 𝑐)) |
23 | 22 | ralbidv 3121 |
. . . . 5
⊢ (𝑊 = if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉) → (∀𝑥 ∈ (BaseSet‘if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉))∃𝑐 ∈
ℝ ∀𝑡 ∈
𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ↔ ∀𝑥 ∈ (BaseSet‘if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉))∃𝑐 ∈
ℝ ∀𝑡 ∈
𝑇
((normCV‘if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉))‘(𝑡‘𝑥)) ≤ 𝑐)) |
24 | | oveq2 7275 |
. . . . . . . 8
⊢ (𝑊 = if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉) → (if(𝑈
∈ CBan, 𝑈,
〈〈 + , · 〉, abs〉) normOpOLD 𝑊) = (if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) normOpOLD if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉))) |
25 | 24 | fveq1d 6768 |
. . . . . . 7
⊢ (𝑊 = if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉) → ((if(𝑈
∈ CBan, 𝑈,
〈〈 + , · 〉, abs〉) normOpOLD 𝑊)‘𝑡) = ((if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) normOpOLD if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉))‘𝑡)) |
26 | 25 | breq1d 5083 |
. . . . . 6
⊢ (𝑊 = if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉) → (((if(𝑈
∈ CBan, 𝑈,
〈〈 + , · 〉, abs〉) normOpOLD 𝑊)‘𝑡) ≤ 𝑑 ↔ ((if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) normOpOLD if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉))‘𝑡) ≤
𝑑)) |
27 | 26 | rexralbidv 3228 |
. . . . 5
⊢ (𝑊 = if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉) → (∃𝑑
∈ ℝ ∀𝑡
∈ 𝑇 ((if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) normOpOLD 𝑊)‘𝑡) ≤ 𝑑 ↔ ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 ((if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) normOpOLD if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉))‘𝑡) ≤
𝑑)) |
28 | 23, 27 | bibi12d 346 |
. . . 4
⊢ (𝑊 = 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 | 16, 28 | imbi12d 345 |
. . 3
⊢ (𝑊 = 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 2738 |
. . . 4
⊢
(BaseSet‘if(𝑈
∈ CBan, 𝑈,
〈〈 + , · 〉, abs〉)) = (BaseSet‘if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉)) |
31 | | eqid 2738 |
. . . 4
⊢
(normCV‘if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉)) = (normCV‘if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉)) |
32 | | eqid 2738 |
. . . 4
⊢
(IndMet‘if(𝑈
∈ CBan, 𝑈,
〈〈 + , · 〉, abs〉)) = (IndMet‘if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉)) |
33 | | eqid 2738 |
. . . 4
⊢
(MetOpen‘(IndMet‘if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉))) = (MetOpen‘(IndMet‘if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉))) |
34 | | eqid 2738 |
. . . . . 6
⊢
〈〈 + , · 〉, abs〉 = 〈〈 + , ·
〉, abs〉 |
35 | 34 | cnbn 29239 |
. . . . 5
⊢
〈〈 + , · 〉, abs〉 ∈ CBan |
36 | 35 | elimel 4528 |
. . . 4
⊢ if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) ∈ CBan |
37 | | elimnvu 29054 |
. . . 4
⊢ if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , ·
〉, abs〉) ∈ NrmCVec |
38 | | id 22 |
. . . 4
⊢ (𝑇 ⊆ (if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) BLnOp if(𝑊
∈ NrmCVec, 𝑊,
〈〈 + , · 〉, abs〉)) → 𝑇 ⊆ (if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) BLnOp if(𝑊
∈ NrmCVec, 𝑊,
〈〈 + , · 〉, abs〉))) |
39 | 30, 31, 32, 33, 36, 37, 38 | ubthlem3 29242 |
. . 3
⊢ (𝑇 ⊆ (if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) BLnOp if(𝑊
∈ NrmCVec, 𝑊,
〈〈 + , · 〉, abs〉)) → (∀𝑥 ∈ (BaseSet‘if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉))∃𝑐 ∈
ℝ ∀𝑡 ∈
𝑇
((normCV‘if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉))‘(𝑡‘𝑥)) ≤ 𝑐 ↔ ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 ((if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) normOpOLD if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉))‘𝑡) ≤
𝑑)) |
40 | 14, 29, 39 | dedth2h 4518 |
. 2
⊢ ((𝑈 ∈ CBan ∧ 𝑊 ∈ NrmCVec) → (𝑇 ⊆ (𝑈 BLnOp 𝑊) → (∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ↔ ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑀‘𝑡) ≤ 𝑑))) |
41 | 40 | 3impia 1116 |
1
⊢ ((𝑈 ∈ CBan ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ⊆ (𝑈 BLnOp 𝑊)) → (∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ↔ ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑀‘𝑡) ≤ 𝑑)) |