Proof of Theorem isblo3i
| Step | Hyp | Ref
| Expression |
| 1 | | isblo3i.u |
. . . 4
⊢ 𝑈 ∈ NrmCVec |
| 2 | | isblo3i.w |
. . . 4
⊢ 𝑊 ∈ NrmCVec |
| 3 | | isblo3i.4 |
. . . . 5
⊢ 𝐿 = (𝑈 LnOp 𝑊) |
| 4 | | isblo3i.5 |
. . . . 5
⊢ 𝐵 = (𝑈 BLnOp 𝑊) |
| 5 | 3, 4 | bloln 30803 |
. . . 4
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵) → 𝑇 ∈ 𝐿) |
| 6 | 1, 2, 5 | mp3an12 1453 |
. . 3
⊢ (𝑇 ∈ 𝐵 → 𝑇 ∈ 𝐿) |
| 7 | | isblo3i.1 |
. . . . . 6
⊢ 𝑋 = (BaseSet‘𝑈) |
| 8 | | eqid 2737 |
. . . . . 6
⊢
(BaseSet‘𝑊) =
(BaseSet‘𝑊) |
| 9 | | eqid 2737 |
. . . . . 6
⊢ (𝑈 normOpOLD 𝑊) = (𝑈 normOpOLD 𝑊) |
| 10 | 7, 8, 9, 4 | nmblore 30805 |
. . . . 5
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵) → ((𝑈 normOpOLD 𝑊)‘𝑇) ∈ ℝ) |
| 11 | 1, 2, 10 | mp3an12 1453 |
. . . 4
⊢ (𝑇 ∈ 𝐵 → ((𝑈 normOpOLD 𝑊)‘𝑇) ∈ ℝ) |
| 12 | | isblo3i.m |
. . . . . 6
⊢ 𝑀 =
(normCV‘𝑈) |
| 13 | | isblo3i.n |
. . . . . 6
⊢ 𝑁 =
(normCV‘𝑊) |
| 14 | 7, 12, 13, 9, 4, 1,
2 | nmblolbi 30819 |
. . . . 5
⊢ ((𝑇 ∈ 𝐵 ∧ 𝑦 ∈ 𝑋) → (𝑁‘(𝑇‘𝑦)) ≤ (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑀‘𝑦))) |
| 15 | 14 | ralrimiva 3146 |
. . . 4
⊢ (𝑇 ∈ 𝐵 → ∀𝑦 ∈ 𝑋 (𝑁‘(𝑇‘𝑦)) ≤ (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑀‘𝑦))) |
| 16 | | oveq1 7438 |
. . . . . . 7
⊢ (𝑥 = ((𝑈 normOpOLD 𝑊)‘𝑇) → (𝑥 · (𝑀‘𝑦)) = (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑀‘𝑦))) |
| 17 | 16 | breq2d 5155 |
. . . . . 6
⊢ (𝑥 = ((𝑈 normOpOLD 𝑊)‘𝑇) → ((𝑁‘(𝑇‘𝑦)) ≤ (𝑥 · (𝑀‘𝑦)) ↔ (𝑁‘(𝑇‘𝑦)) ≤ (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑀‘𝑦)))) |
| 18 | 17 | ralbidv 3178 |
. . . . 5
⊢ (𝑥 = ((𝑈 normOpOLD 𝑊)‘𝑇) → (∀𝑦 ∈ 𝑋 (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 · (𝑀‘𝑦)) ↔ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑇‘𝑦)) ≤ (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑀‘𝑦)))) |
| 19 | 18 | rspcev 3622 |
. . . 4
⊢ ((((𝑈 normOpOLD 𝑊)‘𝑇) ∈ ℝ ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑇‘𝑦)) ≤ (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑀‘𝑦))) → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 · (𝑀‘𝑦))) |
| 20 | 11, 15, 19 | syl2anc 584 |
. . 3
⊢ (𝑇 ∈ 𝐵 → ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 · (𝑀‘𝑦))) |
| 21 | 6, 20 | jca 511 |
. 2
⊢ (𝑇 ∈ 𝐵 → (𝑇 ∈ 𝐿 ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 · (𝑀‘𝑦)))) |
| 22 | | simp1 1137 |
. . . . 5
⊢ ((𝑇 ∈ 𝐿 ∧ 𝑥 ∈ ℝ ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 · (𝑀‘𝑦))) → 𝑇 ∈ 𝐿) |
| 23 | 7, 8, 3 | lnof 30774 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → 𝑇:𝑋⟶(BaseSet‘𝑊)) |
| 24 | 1, 2, 23 | mp3an12 1453 |
. . . . . 6
⊢ (𝑇 ∈ 𝐿 → 𝑇:𝑋⟶(BaseSet‘𝑊)) |
| 25 | 7, 8, 9 | nmoxr 30785 |
. . . . . . . . 9
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶(BaseSet‘𝑊)) → ((𝑈 normOpOLD 𝑊)‘𝑇) ∈
ℝ*) |
| 26 | 1, 2, 25 | mp3an12 1453 |
. . . . . . . 8
⊢ (𝑇:𝑋⟶(BaseSet‘𝑊) → ((𝑈 normOpOLD 𝑊)‘𝑇) ∈
ℝ*) |
| 27 | 26 | 3ad2ant1 1134 |
. . . . . . 7
⊢ ((𝑇:𝑋⟶(BaseSet‘𝑊) ∧ 𝑥 ∈ ℝ ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 · (𝑀‘𝑦))) → ((𝑈 normOpOLD 𝑊)‘𝑇) ∈
ℝ*) |
| 28 | | recn 11245 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ → 𝑥 ∈
ℂ) |
| 29 | 28 | abscld 15475 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ →
(abs‘𝑥) ∈
ℝ) |
| 30 | 29 | rexrd 11311 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ →
(abs‘𝑥) ∈
ℝ*) |
| 31 | 30 | 3ad2ant2 1135 |
. . . . . . 7
⊢ ((𝑇:𝑋⟶(BaseSet‘𝑊) ∧ 𝑥 ∈ ℝ ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 · (𝑀‘𝑦))) → (abs‘𝑥) ∈
ℝ*) |
| 32 | | pnfxr 11315 |
. . . . . . . 8
⊢ +∞
∈ ℝ* |
| 33 | 32 | a1i 11 |
. . . . . . 7
⊢ ((𝑇:𝑋⟶(BaseSet‘𝑊) ∧ 𝑥 ∈ ℝ ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 · (𝑀‘𝑦))) → +∞ ∈
ℝ*) |
| 34 | 7, 8, 12, 13, 9, 1, 2 | nmoub3i 30792 |
. . . . . . 7
⊢ ((𝑇:𝑋⟶(BaseSet‘𝑊) ∧ 𝑥 ∈ ℝ ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 · (𝑀‘𝑦))) → ((𝑈 normOpOLD 𝑊)‘𝑇) ≤ (abs‘𝑥)) |
| 35 | | ltpnf 13162 |
. . . . . . . . 9
⊢
((abs‘𝑥)
∈ ℝ → (abs‘𝑥) < +∞) |
| 36 | 29, 35 | syl 17 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ →
(abs‘𝑥) <
+∞) |
| 37 | 36 | 3ad2ant2 1135 |
. . . . . . 7
⊢ ((𝑇:𝑋⟶(BaseSet‘𝑊) ∧ 𝑥 ∈ ℝ ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 · (𝑀‘𝑦))) → (abs‘𝑥) < +∞) |
| 38 | 27, 31, 33, 34, 37 | xrlelttrd 13202 |
. . . . . 6
⊢ ((𝑇:𝑋⟶(BaseSet‘𝑊) ∧ 𝑥 ∈ ℝ ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 · (𝑀‘𝑦))) → ((𝑈 normOpOLD 𝑊)‘𝑇) < +∞) |
| 39 | 24, 38 | syl3an1 1164 |
. . . . 5
⊢ ((𝑇 ∈ 𝐿 ∧ 𝑥 ∈ ℝ ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 · (𝑀‘𝑦))) → ((𝑈 normOpOLD 𝑊)‘𝑇) < +∞) |
| 40 | 9, 3, 4 | isblo 30801 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑇 ∈ 𝐵 ↔ (𝑇 ∈ 𝐿 ∧ ((𝑈 normOpOLD 𝑊)‘𝑇) < +∞))) |
| 41 | 1, 2, 40 | mp2an 692 |
. . . . 5
⊢ (𝑇 ∈ 𝐵 ↔ (𝑇 ∈ 𝐿 ∧ ((𝑈 normOpOLD 𝑊)‘𝑇) < +∞)) |
| 42 | 22, 39, 41 | sylanbrc 583 |
. . . 4
⊢ ((𝑇 ∈ 𝐿 ∧ 𝑥 ∈ ℝ ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 · (𝑀‘𝑦))) → 𝑇 ∈ 𝐵) |
| 43 | 42 | rexlimdv3a 3159 |
. . 3
⊢ (𝑇 ∈ 𝐿 → (∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 · (𝑀‘𝑦)) → 𝑇 ∈ 𝐵)) |
| 44 | 43 | imp 406 |
. 2
⊢ ((𝑇 ∈ 𝐿 ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 · (𝑀‘𝑦))) → 𝑇 ∈ 𝐵) |
| 45 | 21, 44 | impbii 209 |
1
⊢ (𝑇 ∈ 𝐵 ↔ (𝑇 ∈ 𝐿 ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 · (𝑀‘𝑦)))) |