| Step | Hyp | Ref
| Expression |
| 1 | | blocni.u |
. . . 4
⊢ 𝑈 ∈ NrmCVec |
| 2 | | eqid 2737 |
. . . . 5
⊢
(BaseSet‘𝑈) =
(BaseSet‘𝑈) |
| 3 | | eqid 2737 |
. . . . 5
⊢
(0vec‘𝑈) = (0vec‘𝑈) |
| 4 | 2, 3 | nvzcl 30653 |
. . . 4
⊢ (𝑈 ∈ NrmCVec →
(0vec‘𝑈)
∈ (BaseSet‘𝑈)) |
| 5 | 1, 4 | ax-mp 5 |
. . 3
⊢
(0vec‘𝑈) ∈ (BaseSet‘𝑈) |
| 6 | | blocni.8 |
. . . . . . . . . 10
⊢ 𝐶 = (IndMet‘𝑈) |
| 7 | 2, 6 | imsmet 30710 |
. . . . . . . . 9
⊢ (𝑈 ∈ NrmCVec → 𝐶 ∈
(Met‘(BaseSet‘𝑈))) |
| 8 | 1, 7 | ax-mp 5 |
. . . . . . . 8
⊢ 𝐶 ∈
(Met‘(BaseSet‘𝑈)) |
| 9 | | metxmet 24344 |
. . . . . . . 8
⊢ (𝐶 ∈
(Met‘(BaseSet‘𝑈)) → 𝐶 ∈
(∞Met‘(BaseSet‘𝑈))) |
| 10 | 8, 9 | ax-mp 5 |
. . . . . . 7
⊢ 𝐶 ∈
(∞Met‘(BaseSet‘𝑈)) |
| 11 | | blocni.j |
. . . . . . . 8
⊢ 𝐽 = (MetOpen‘𝐶) |
| 12 | 11 | mopntopon 24449 |
. . . . . . 7
⊢ (𝐶 ∈
(∞Met‘(BaseSet‘𝑈)) → 𝐽 ∈ (TopOn‘(BaseSet‘𝑈))) |
| 13 | 10, 12 | ax-mp 5 |
. . . . . 6
⊢ 𝐽 ∈
(TopOn‘(BaseSet‘𝑈)) |
| 14 | 13 | toponunii 22922 |
. . . . 5
⊢
(BaseSet‘𝑈) =
∪ 𝐽 |
| 15 | 14 | cncnpi 23286 |
. . . 4
⊢ ((𝑇 ∈ (𝐽 Cn 𝐾) ∧ (0vec‘𝑈) ∈ (BaseSet‘𝑈)) → 𝑇 ∈ ((𝐽 CnP 𝐾)‘(0vec‘𝑈))) |
| 16 | 5, 15 | mpan2 691 |
. . 3
⊢ (𝑇 ∈ (𝐽 Cn 𝐾) → 𝑇 ∈ ((𝐽 CnP 𝐾)‘(0vec‘𝑈))) |
| 17 | | blocni.d |
. . . 4
⊢ 𝐷 = (IndMet‘𝑊) |
| 18 | | blocni.k |
. . . 4
⊢ 𝐾 = (MetOpen‘𝐷) |
| 19 | | blocni.4 |
. . . 4
⊢ 𝐿 = (𝑈 LnOp 𝑊) |
| 20 | | blocni.5 |
. . . 4
⊢ 𝐵 = (𝑈 BLnOp 𝑊) |
| 21 | | blocni.w |
. . . 4
⊢ 𝑊 ∈ NrmCVec |
| 22 | | blocni.l |
. . . 4
⊢ 𝑇 ∈ 𝐿 |
| 23 | 6, 17, 11, 18, 19, 20, 1, 21, 22, 2 | blocnilem 30823 |
. . 3
⊢
(((0vec‘𝑈) ∈ (BaseSet‘𝑈) ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)‘(0vec‘𝑈))) → 𝑇 ∈ 𝐵) |
| 24 | 5, 16, 23 | sylancr 587 |
. 2
⊢ (𝑇 ∈ (𝐽 Cn 𝐾) → 𝑇 ∈ 𝐵) |
| 25 | | eleq1 2829 |
. . 3
⊢ (𝑇 = (𝑈 0op 𝑊) → (𝑇 ∈ (𝐽 Cn 𝐾) ↔ (𝑈 0op 𝑊) ∈ (𝐽 Cn 𝐾))) |
| 26 | | simprr 773 |
. . . . . . . 8
⊢ (((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) → 𝑦 ∈
ℝ+) |
| 27 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(BaseSet‘𝑊) =
(BaseSet‘𝑊) |
| 28 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢ (𝑈 normOpOLD 𝑊) = (𝑈 normOpOLD 𝑊) |
| 29 | 2, 27, 28, 20 | nmblore 30805 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵) → ((𝑈 normOpOLD 𝑊)‘𝑇) ∈ ℝ) |
| 30 | 1, 21, 29 | mp3an12 1453 |
. . . . . . . . . . 11
⊢ (𝑇 ∈ 𝐵 → ((𝑈 normOpOLD 𝑊)‘𝑇) ∈ ℝ) |
| 31 | | eqid 2737 |
. . . . . . . . . . . . . 14
⊢ (𝑈 0op 𝑊) = (𝑈 0op 𝑊) |
| 32 | 28, 31, 19 | nmlnogt0 30816 |
. . . . . . . . . . . . 13
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → (𝑇 ≠ (𝑈 0op 𝑊) ↔ 0 < ((𝑈 normOpOLD 𝑊)‘𝑇))) |
| 33 | 1, 21, 22, 32 | mp3an 1463 |
. . . . . . . . . . . 12
⊢ (𝑇 ≠ (𝑈 0op 𝑊) ↔ 0 < ((𝑈 normOpOLD 𝑊)‘𝑇)) |
| 34 | 33 | biimpi 216 |
. . . . . . . . . . 11
⊢ (𝑇 ≠ (𝑈 0op 𝑊) → 0 < ((𝑈 normOpOLD 𝑊)‘𝑇)) |
| 35 | 30, 34 | anim12i 613 |
. . . . . . . . . 10
⊢ ((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) → (((𝑈 normOpOLD 𝑊)‘𝑇) ∈ ℝ ∧ 0 < ((𝑈 normOpOLD 𝑊)‘𝑇))) |
| 36 | | elrp 13036 |
. . . . . . . . . 10
⊢ (((𝑈 normOpOLD 𝑊)‘𝑇) ∈ ℝ+ ↔ (((𝑈 normOpOLD 𝑊)‘𝑇) ∈ ℝ ∧ 0 < ((𝑈 normOpOLD 𝑊)‘𝑇))) |
| 37 | 35, 36 | sylibr 234 |
. . . . . . . . 9
⊢ ((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) → ((𝑈 normOpOLD 𝑊)‘𝑇) ∈
ℝ+) |
| 38 | 37 | adantr 480 |
. . . . . . . 8
⊢ (((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) → ((𝑈 normOpOLD 𝑊)‘𝑇) ∈
ℝ+) |
| 39 | 26, 38 | rpdivcld 13094 |
. . . . . . 7
⊢ (((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) → (𝑦 / ((𝑈 normOpOLD 𝑊)‘𝑇)) ∈
ℝ+) |
| 40 | | simprl 771 |
. . . . . . . . . . 11
⊢ (((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) → 𝑥 ∈ (BaseSet‘𝑈)) |
| 41 | | metcl 24342 |
. . . . . . . . . . . 12
⊢ ((𝐶 ∈
(Met‘(BaseSet‘𝑈)) ∧ 𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → (𝑥𝐶𝑤) ∈ ℝ) |
| 42 | 8, 41 | mp3an1 1450 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → (𝑥𝐶𝑤) ∈ ℝ) |
| 43 | 40, 42 | sylan 580 |
. . . . . . . . . 10
⊢ ((((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → (𝑥𝐶𝑤) ∈ ℝ) |
| 44 | | simplrr 778 |
. . . . . . . . . . 11
⊢ ((((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → 𝑦 ∈ ℝ+) |
| 45 | 44 | rpred 13077 |
. . . . . . . . . 10
⊢ ((((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → 𝑦 ∈ ℝ) |
| 46 | 35 | ad2antrr 726 |
. . . . . . . . . 10
⊢ ((((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → (((𝑈 normOpOLD 𝑊)‘𝑇) ∈ ℝ ∧ 0 < ((𝑈 normOpOLD 𝑊)‘𝑇))) |
| 47 | | ltmuldiv2 12142 |
. . . . . . . . . 10
⊢ (((𝑥𝐶𝑤) ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ (((𝑈 normOpOLD 𝑊)‘𝑇) ∈ ℝ ∧ 0 < ((𝑈 normOpOLD 𝑊)‘𝑇))) → ((((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) < 𝑦 ↔ (𝑥𝐶𝑤) < (𝑦 / ((𝑈 normOpOLD 𝑊)‘𝑇)))) |
| 48 | 43, 45, 46, 47 | syl3anc 1373 |
. . . . . . . . 9
⊢ ((((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → ((((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) < 𝑦 ↔ (𝑥𝐶𝑤) < (𝑦 / ((𝑈 normOpOLD 𝑊)‘𝑇)))) |
| 49 | | id 22 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ 𝐵 ∧ 𝑥 ∈ (BaseSet‘𝑈)) → (𝑇 ∈ 𝐵 ∧ 𝑥 ∈ (BaseSet‘𝑈))) |
| 50 | 49 | ad2ant2r 747 |
. . . . . . . . . . 11
⊢ (((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) → (𝑇 ∈ 𝐵 ∧ 𝑥 ∈ (BaseSet‘𝑈))) |
| 51 | 2, 27, 6, 17, 28, 20, 1, 21 | blometi 30822 |
. . . . . . . . . . . 12
⊢ ((𝑇 ∈ 𝐵 ∧ 𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) ≤ (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤))) |
| 52 | 51 | 3expa 1119 |
. . . . . . . . . . 11
⊢ (((𝑇 ∈ 𝐵 ∧ 𝑥 ∈ (BaseSet‘𝑈)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) ≤ (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤))) |
| 53 | 50, 52 | sylan 580 |
. . . . . . . . . 10
⊢ ((((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) ≤ (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤))) |
| 54 | 2, 27, 19 | lnof 30774 |
. . . . . . . . . . . . . . 15
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → 𝑇:(BaseSet‘𝑈)⟶(BaseSet‘𝑊)) |
| 55 | 1, 21, 22, 54 | mp3an 1463 |
. . . . . . . . . . . . . 14
⊢ 𝑇:(BaseSet‘𝑈)⟶(BaseSet‘𝑊) |
| 56 | 55 | ffvelcdmi 7103 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ (BaseSet‘𝑈) → (𝑇‘𝑥) ∈ (BaseSet‘𝑊)) |
| 57 | 55 | ffvelcdmi 7103 |
. . . . . . . . . . . . 13
⊢ (𝑤 ∈ (BaseSet‘𝑈) → (𝑇‘𝑤) ∈ (BaseSet‘𝑊)) |
| 58 | 27, 17 | imsmet 30710 |
. . . . . . . . . . . . . . 15
⊢ (𝑊 ∈ NrmCVec → 𝐷 ∈
(Met‘(BaseSet‘𝑊))) |
| 59 | 21, 58 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢ 𝐷 ∈
(Met‘(BaseSet‘𝑊)) |
| 60 | | metcl 24342 |
. . . . . . . . . . . . . 14
⊢ ((𝐷 ∈
(Met‘(BaseSet‘𝑊)) ∧ (𝑇‘𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑇‘𝑤) ∈ (BaseSet‘𝑊)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) ∈ ℝ) |
| 61 | 59, 60 | mp3an1 1450 |
. . . . . . . . . . . . 13
⊢ (((𝑇‘𝑥) ∈ (BaseSet‘𝑊) ∧ (𝑇‘𝑤) ∈ (BaseSet‘𝑊)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) ∈ ℝ) |
| 62 | 56, 57, 61 | syl2an 596 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) ∈ ℝ) |
| 63 | 40, 62 | sylan 580 |
. . . . . . . . . . 11
⊢ ((((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) ∈ ℝ) |
| 64 | | remulcl 11240 |
. . . . . . . . . . . . . . 15
⊢ ((((𝑈 normOpOLD 𝑊)‘𝑇) ∈ ℝ ∧ (𝑥𝐶𝑤) ∈ ℝ) → (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) ∈ ℝ) |
| 65 | 30, 42, 64 | syl2an 596 |
. . . . . . . . . . . . . 14
⊢ ((𝑇 ∈ 𝐵 ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑤 ∈ (BaseSet‘𝑈))) → (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) ∈ ℝ) |
| 66 | 65 | anassrs 467 |
. . . . . . . . . . . . 13
⊢ (((𝑇 ∈ 𝐵 ∧ 𝑥 ∈ (BaseSet‘𝑈)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) ∈ ℝ) |
| 67 | 66 | adantllr 719 |
. . . . . . . . . . . 12
⊢ ((((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ 𝑥 ∈ (BaseSet‘𝑈)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) ∈ ℝ) |
| 68 | 67 | adantlrr 721 |
. . . . . . . . . . 11
⊢ ((((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) ∈ ℝ) |
| 69 | | lelttr 11351 |
. . . . . . . . . . 11
⊢ ((((𝑇‘𝑥)𝐷(𝑇‘𝑤)) ∈ ℝ ∧ (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) ∈ ℝ ∧ 𝑦 ∈ ℝ) → ((((𝑇‘𝑥)𝐷(𝑇‘𝑤)) ≤ (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) ∧ (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) < 𝑦) → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) < 𝑦)) |
| 70 | 63, 68, 45, 69 | syl3anc 1373 |
. . . . . . . . . 10
⊢ ((((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → ((((𝑇‘𝑥)𝐷(𝑇‘𝑤)) ≤ (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) ∧ (((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) < 𝑦) → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) < 𝑦)) |
| 71 | 53, 70 | mpand 695 |
. . . . . . . . 9
⊢ ((((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → ((((𝑈 normOpOLD 𝑊)‘𝑇) · (𝑥𝐶𝑤)) < 𝑦 → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) < 𝑦)) |
| 72 | 48, 71 | sylbird 260 |
. . . . . . . 8
⊢ ((((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) ∧ 𝑤 ∈ (BaseSet‘𝑈)) → ((𝑥𝐶𝑤) < (𝑦 / ((𝑈 normOpOLD 𝑊)‘𝑇)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) < 𝑦)) |
| 73 | 72 | ralrimiva 3146 |
. . . . . . 7
⊢ (((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) →
∀𝑤 ∈
(BaseSet‘𝑈)((𝑥𝐶𝑤) < (𝑦 / ((𝑈 normOpOLD 𝑊)‘𝑇)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) < 𝑦)) |
| 74 | | breq2 5147 |
. . . . . . . 8
⊢ (𝑧 = (𝑦 / ((𝑈 normOpOLD 𝑊)‘𝑇)) → ((𝑥𝐶𝑤) < 𝑧 ↔ (𝑥𝐶𝑤) < (𝑦 / ((𝑈 normOpOLD 𝑊)‘𝑇)))) |
| 75 | 74 | rspceaimv 3628 |
. . . . . . 7
⊢ (((𝑦 / ((𝑈 normOpOLD 𝑊)‘𝑇)) ∈ ℝ+ ∧
∀𝑤 ∈
(BaseSet‘𝑈)((𝑥𝐶𝑤) < (𝑦 / ((𝑈 normOpOLD 𝑊)‘𝑇)) → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) < 𝑦)) → ∃𝑧 ∈ ℝ+ ∀𝑤 ∈ (BaseSet‘𝑈)((𝑥𝐶𝑤) < 𝑧 → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) < 𝑦)) |
| 76 | 39, 73, 75 | syl2anc 584 |
. . . . . 6
⊢ (((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) ∧ (𝑥 ∈ (BaseSet‘𝑈) ∧ 𝑦 ∈ ℝ+)) →
∃𝑧 ∈
ℝ+ ∀𝑤 ∈ (BaseSet‘𝑈)((𝑥𝐶𝑤) < 𝑧 → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) < 𝑦)) |
| 77 | 76 | ralrimivva 3202 |
. . . . 5
⊢ ((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) → ∀𝑥 ∈ (BaseSet‘𝑈)∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈
(BaseSet‘𝑈)((𝑥𝐶𝑤) < 𝑧 → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) < 𝑦)) |
| 78 | 77, 55 | jctil 519 |
. . . 4
⊢ ((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) → (𝑇:(BaseSet‘𝑈)⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈ (BaseSet‘𝑈)∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈
(BaseSet‘𝑈)((𝑥𝐶𝑤) < 𝑧 → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) < 𝑦))) |
| 79 | | metxmet 24344 |
. . . . . 6
⊢ (𝐷 ∈
(Met‘(BaseSet‘𝑊)) → 𝐷 ∈
(∞Met‘(BaseSet‘𝑊))) |
| 80 | 59, 79 | ax-mp 5 |
. . . . 5
⊢ 𝐷 ∈
(∞Met‘(BaseSet‘𝑊)) |
| 81 | 11, 18 | metcn 24556 |
. . . . 5
⊢ ((𝐶 ∈
(∞Met‘(BaseSet‘𝑈)) ∧ 𝐷 ∈
(∞Met‘(BaseSet‘𝑊))) → (𝑇 ∈ (𝐽 Cn 𝐾) ↔ (𝑇:(BaseSet‘𝑈)⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈ (BaseSet‘𝑈)∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈
(BaseSet‘𝑈)((𝑥𝐶𝑤) < 𝑧 → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) < 𝑦)))) |
| 82 | 10, 80, 81 | mp2an 692 |
. . . 4
⊢ (𝑇 ∈ (𝐽 Cn 𝐾) ↔ (𝑇:(BaseSet‘𝑈)⟶(BaseSet‘𝑊) ∧ ∀𝑥 ∈ (BaseSet‘𝑈)∀𝑦 ∈ ℝ+ ∃𝑧 ∈ ℝ+
∀𝑤 ∈
(BaseSet‘𝑈)((𝑥𝐶𝑤) < 𝑧 → ((𝑇‘𝑥)𝐷(𝑇‘𝑤)) < 𝑦))) |
| 83 | 78, 82 | sylibr 234 |
. . 3
⊢ ((𝑇 ∈ 𝐵 ∧ 𝑇 ≠ (𝑈 0op 𝑊)) → 𝑇 ∈ (𝐽 Cn 𝐾)) |
| 84 | | eqid 2737 |
. . . . . . 7
⊢
(0vec‘𝑊) = (0vec‘𝑊) |
| 85 | 2, 84, 31 | 0ofval 30806 |
. . . . . 6
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑈 0op 𝑊) = ((BaseSet‘𝑈) ×
{(0vec‘𝑊)})) |
| 86 | 1, 21, 85 | mp2an 692 |
. . . . 5
⊢ (𝑈 0op 𝑊) = ((BaseSet‘𝑈) ×
{(0vec‘𝑊)}) |
| 87 | 18 | mopntopon 24449 |
. . . . . . 7
⊢ (𝐷 ∈
(∞Met‘(BaseSet‘𝑊)) → 𝐾 ∈ (TopOn‘(BaseSet‘𝑊))) |
| 88 | 80, 87 | ax-mp 5 |
. . . . . 6
⊢ 𝐾 ∈
(TopOn‘(BaseSet‘𝑊)) |
| 89 | 27, 84 | nvzcl 30653 |
. . . . . . 7
⊢ (𝑊 ∈ NrmCVec →
(0vec‘𝑊)
∈ (BaseSet‘𝑊)) |
| 90 | 21, 89 | ax-mp 5 |
. . . . . 6
⊢
(0vec‘𝑊) ∈ (BaseSet‘𝑊) |
| 91 | | cnconst2 23291 |
. . . . . 6
⊢ ((𝐽 ∈
(TopOn‘(BaseSet‘𝑈)) ∧ 𝐾 ∈ (TopOn‘(BaseSet‘𝑊)) ∧
(0vec‘𝑊)
∈ (BaseSet‘𝑊))
→ ((BaseSet‘𝑈)
× {(0vec‘𝑊)}) ∈ (𝐽 Cn 𝐾)) |
| 92 | 13, 88, 90, 91 | mp3an 1463 |
. . . . 5
⊢
((BaseSet‘𝑈)
× {(0vec‘𝑊)}) ∈ (𝐽 Cn 𝐾) |
| 93 | 86, 92 | eqeltri 2837 |
. . . 4
⊢ (𝑈 0op 𝑊) ∈ (𝐽 Cn 𝐾) |
| 94 | 93 | a1i 11 |
. . 3
⊢ (𝑇 ∈ 𝐵 → (𝑈 0op 𝑊) ∈ (𝐽 Cn 𝐾)) |
| 95 | 25, 83, 94 | pm2.61ne 3027 |
. 2
⊢ (𝑇 ∈ 𝐵 → 𝑇 ∈ (𝐽 Cn 𝐾)) |
| 96 | 24, 95 | impbii 209 |
1
⊢ (𝑇 ∈ (𝐽 Cn 𝐾) ↔ 𝑇 ∈ 𝐵) |