Proof of Theorem ubth
| Step | Hyp | Ref
| Expression |
| 1 | | oveq1 7438 |
. . . . 5
⊢ (𝑈 = if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) → (𝑈 BLnOp
𝑊) = (if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) BLnOp 𝑊)) |
| 2 | 1 | sseq2d 4016 |
. . . 4
⊢ (𝑈 = if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) → (𝑇
⊆ (𝑈 BLnOp 𝑊) ↔ 𝑇 ⊆ (if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) BLnOp 𝑊))) |
| 3 | | ubth.1 |
. . . . . . 7
⊢ 𝑋 = (BaseSet‘𝑈) |
| 4 | | fveq2 6906 |
. . . . . . 7
⊢ (𝑈 = if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) → (BaseSet‘𝑈) = (BaseSet‘if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉))) |
| 5 | 3, 4 | eqtrid 2789 |
. . . . . 6
⊢ (𝑈 = if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) → 𝑋 =
(BaseSet‘if(𝑈 ∈
CBan, 𝑈, 〈〈 + ,
· 〉, abs〉))) |
| 6 | 5 | raleqdv 3326 |
. . . . 5
⊢ (𝑈 = if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) → (∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ↔ ∀𝑥 ∈ (BaseSet‘if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉))∃𝑐 ∈
ℝ ∀𝑡 ∈
𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐)) |
| 7 | | ubth.3 |
. . . . . . . . 9
⊢ 𝑀 = (𝑈 normOpOLD 𝑊) |
| 8 | | oveq1 7438 |
. . . . . . . . 9
⊢ (𝑈 = if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) → (𝑈
normOpOLD 𝑊) =
(if(𝑈 ∈ CBan, 𝑈, 〈〈 + , ·
〉, abs〉) normOpOLD 𝑊)) |
| 9 | 7, 8 | eqtrid 2789 |
. . . . . . . 8
⊢ (𝑈 = if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) → 𝑀 =
(if(𝑈 ∈ CBan, 𝑈, 〈〈 + , ·
〉, abs〉) normOpOLD 𝑊)) |
| 10 | 9 | fveq1d 6908 |
. . . . . . 7
⊢ (𝑈 = if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) → (𝑀‘𝑡) = ((if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) normOpOLD 𝑊)‘𝑡)) |
| 11 | 10 | breq1d 5153 |
. . . . . 6
⊢ (𝑈 = if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) → ((𝑀‘𝑡) ≤ 𝑑 ↔ ((if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) normOpOLD 𝑊)‘𝑡) ≤ 𝑑)) |
| 12 | 11 | rexralbidv 3223 |
. . . . 5
⊢ (𝑈 = if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) → (∃𝑑
∈ ℝ ∀𝑡
∈ 𝑇 (𝑀‘𝑡) ≤ 𝑑 ↔ ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 ((if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) normOpOLD 𝑊)‘𝑡) ≤ 𝑑)) |
| 13 | 6, 12 | bibi12d 345 |
. . . 4
⊢ (𝑈 = if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) → ((∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ↔ ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑀‘𝑡) ≤ 𝑑) ↔ (∀𝑥 ∈ (BaseSet‘if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉))∃𝑐 ∈
ℝ ∀𝑡 ∈
𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ↔ ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 ((if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) normOpOLD 𝑊)‘𝑡) ≤ 𝑑))) |
| 14 | 2, 13 | imbi12d 344 |
. . 3
⊢ (𝑈 = if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) → ((𝑇
⊆ (𝑈 BLnOp 𝑊) → (∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ↔ ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑀‘𝑡) ≤ 𝑑)) ↔ (𝑇 ⊆ (if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) BLnOp 𝑊) →
(∀𝑥 ∈
(BaseSet‘if(𝑈 ∈
CBan, 𝑈, 〈〈 + ,
· 〉, abs〉))∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ↔ ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 ((if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) normOpOLD 𝑊)‘𝑡) ≤ 𝑑)))) |
| 15 | | oveq2 7439 |
. . . . 5
⊢ (𝑊 = if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉) → (if(𝑈
∈ CBan, 𝑈,
〈〈 + , · 〉, abs〉) BLnOp 𝑊) = (if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) BLnOp if(𝑊
∈ NrmCVec, 𝑊,
〈〈 + , · 〉, abs〉))) |
| 16 | 15 | sseq2d 4016 |
. . . 4
⊢ (𝑊 = if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉) → (𝑇
⊆ (if(𝑈 ∈ CBan,
𝑈, 〈〈 + ,
· 〉, abs〉) BLnOp 𝑊) ↔ 𝑇 ⊆ (if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) BLnOp if(𝑊
∈ NrmCVec, 𝑊,
〈〈 + , · 〉, abs〉)))) |
| 17 | | ubth.2 |
. . . . . . . . . 10
⊢ 𝑁 =
(normCV‘𝑊) |
| 18 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑊 = if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉) → (normCV‘𝑊) = (normCV‘if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , ·
〉, abs〉))) |
| 19 | 17, 18 | eqtrid 2789 |
. . . . . . . . 9
⊢ (𝑊 = if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉) → 𝑁 =
(normCV‘if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉))) |
| 20 | 19 | fveq1d 6908 |
. . . . . . . 8
⊢ (𝑊 = if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉) → (𝑁‘(𝑡‘𝑥)) = ((normCV‘if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , ·
〉, abs〉))‘(𝑡‘𝑥))) |
| 21 | 20 | breq1d 5153 |
. . . . . . 7
⊢ (𝑊 = if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉) → ((𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ↔ ((normCV‘if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , ·
〉, abs〉))‘(𝑡‘𝑥)) ≤ 𝑐)) |
| 22 | 21 | rexralbidv 3223 |
. . . . . 6
⊢ (𝑊 = if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉) → (∃𝑐
∈ ℝ ∀𝑡
∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ↔ ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 ((normCV‘if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , ·
〉, abs〉))‘(𝑡‘𝑥)) ≤ 𝑐)) |
| 23 | 22 | ralbidv 3178 |
. . . . 5
⊢ (𝑊 = if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉) → (∀𝑥 ∈ (BaseSet‘if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉))∃𝑐 ∈
ℝ ∀𝑡 ∈
𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ↔ ∀𝑥 ∈ (BaseSet‘if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉))∃𝑐 ∈
ℝ ∀𝑡 ∈
𝑇
((normCV‘if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉))‘(𝑡‘𝑥)) ≤ 𝑐)) |
| 24 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑊 = if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉) → (if(𝑈
∈ CBan, 𝑈,
〈〈 + , · 〉, abs〉) normOpOLD 𝑊) = (if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) normOpOLD if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉))) |
| 25 | 24 | fveq1d 6908 |
. . . . . . 7
⊢ (𝑊 = if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉) → ((if(𝑈
∈ CBan, 𝑈,
〈〈 + , · 〉, abs〉) normOpOLD 𝑊)‘𝑡) = ((if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) normOpOLD if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉))‘𝑡)) |
| 26 | 25 | breq1d 5153 |
. . . . . 6
⊢ (𝑊 = if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉) → (((if(𝑈
∈ CBan, 𝑈,
〈〈 + , · 〉, abs〉) normOpOLD 𝑊)‘𝑡) ≤ 𝑑 ↔ ((if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) normOpOLD if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉))‘𝑡) ≤
𝑑)) |
| 27 | 26 | rexralbidv 3223 |
. . . . 5
⊢ (𝑊 = if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉) → (∃𝑑
∈ ℝ ∀𝑡
∈ 𝑇 ((if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) normOpOLD 𝑊)‘𝑡) ≤ 𝑑 ↔ ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 ((if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) normOpOLD if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉))‘𝑡) ≤
𝑑)) |
| 28 | 23, 27 | bibi12d 345 |
. . . 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 344 |
. . 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 2737 |
. . . 4
⊢
(BaseSet‘if(𝑈
∈ CBan, 𝑈,
〈〈 + , · 〉, abs〉)) = (BaseSet‘if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉)) |
| 31 | | eqid 2737 |
. . . 4
⊢
(normCV‘if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉)) = (normCV‘if(𝑊 ∈ NrmCVec, 𝑊, 〈〈 + , · 〉,
abs〉)) |
| 32 | | eqid 2737 |
. . . 4
⊢
(IndMet‘if(𝑈
∈ CBan, 𝑈,
〈〈 + , · 〉, abs〉)) = (IndMet‘if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉)) |
| 33 | | eqid 2737 |
. . . 4
⊢
(MetOpen‘(IndMet‘if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉))) = (MetOpen‘(IndMet‘if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉))) |
| 34 | | eqid 2737 |
. . . . . 6
⊢
〈〈 + , · 〉, abs〉 = 〈〈 + , ·
〉, abs〉 |
| 35 | 34 | cnbn 30888 |
. . . . 5
⊢
〈〈 + , · 〉, abs〉 ∈ CBan |
| 36 | 35 | elimel 4595 |
. . . 4
⊢ if(𝑈 ∈ CBan, 𝑈, 〈〈 + , · 〉,
abs〉) ∈ CBan |
| 37 | | elimnvu 30703 |
. . . 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 30891 |
. . 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 4585 |
. 2
⊢ ((𝑈 ∈ CBan ∧ 𝑊 ∈ NrmCVec) → (𝑇 ⊆ (𝑈 BLnOp 𝑊) → (∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ↔ ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑀‘𝑡) ≤ 𝑑))) |
| 41 | 40 | 3impia 1118 |
1
⊢ ((𝑈 ∈ CBan ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ⊆ (𝑈 BLnOp 𝑊)) → (∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ↔ ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑀‘𝑡) ≤ 𝑑)) |