Step | Hyp | Ref
| Expression |
1 | | fveq1 6102 |
. . . . . . . . . 10
⊢ (𝑢 = 𝑡 → (𝑢‘𝑧) = (𝑡‘𝑧)) |
2 | 1 | fveq2d 6107 |
. . . . . . . . 9
⊢ (𝑢 = 𝑡 → (𝑁‘(𝑢‘𝑧)) = (𝑁‘(𝑡‘𝑧))) |
3 | 2 | breq1d 4593 |
. . . . . . . 8
⊢ (𝑢 = 𝑡 → ((𝑁‘(𝑢‘𝑧)) ≤ 𝑑 ↔ (𝑁‘(𝑡‘𝑧)) ≤ 𝑑)) |
4 | 3 | cbvralv 3147 |
. . . . . . 7
⊢
(∀𝑢 ∈
𝑇 (𝑁‘(𝑢‘𝑧)) ≤ 𝑑 ↔ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑑) |
5 | | breq2 4587 |
. . . . . . . 8
⊢ (𝑑 = 𝑐 → ((𝑁‘(𝑡‘𝑧)) ≤ 𝑑 ↔ (𝑁‘(𝑡‘𝑧)) ≤ 𝑐)) |
6 | 5 | ralbidv 2969 |
. . . . . . 7
⊢ (𝑑 = 𝑐 → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑑 ↔ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑐)) |
7 | 4, 6 | syl5bb 271 |
. . . . . 6
⊢ (𝑑 = 𝑐 → (∀𝑢 ∈ 𝑇 (𝑁‘(𝑢‘𝑧)) ≤ 𝑑 ↔ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑐)) |
8 | 7 | cbvrexv 3148 |
. . . . 5
⊢
(∃𝑑 ∈
ℝ ∀𝑢 ∈
𝑇 (𝑁‘(𝑢‘𝑧)) ≤ 𝑑 ↔ ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑐) |
9 | | fveq2 6103 |
. . . . . . . 8
⊢ (𝑧 = 𝑥 → (𝑡‘𝑧) = (𝑡‘𝑥)) |
10 | 9 | fveq2d 6107 |
. . . . . . 7
⊢ (𝑧 = 𝑥 → (𝑁‘(𝑡‘𝑧)) = (𝑁‘(𝑡‘𝑥))) |
11 | 10 | breq1d 4593 |
. . . . . 6
⊢ (𝑧 = 𝑥 → ((𝑁‘(𝑡‘𝑧)) ≤ 𝑐 ↔ (𝑁‘(𝑡‘𝑥)) ≤ 𝑐)) |
12 | 11 | rexralbidv 3040 |
. . . . 5
⊢ (𝑧 = 𝑥 → (∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑐 ↔ ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐)) |
13 | 8, 12 | syl5bb 271 |
. . . 4
⊢ (𝑧 = 𝑥 → (∃𝑑 ∈ ℝ ∀𝑢 ∈ 𝑇 (𝑁‘(𝑢‘𝑧)) ≤ 𝑑 ↔ ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐)) |
14 | 13 | cbvralv 3147 |
. . 3
⊢
(∀𝑧 ∈
𝑋 ∃𝑑 ∈ ℝ ∀𝑢 ∈ 𝑇 (𝑁‘(𝑢‘𝑧)) ≤ 𝑑 ↔ ∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐) |
15 | | ubth.1 |
. . . . . 6
⊢ 𝑋 = (BaseSet‘𝑈) |
16 | | ubth.2 |
. . . . . 6
⊢ 𝑁 =
(normCV‘𝑊) |
17 | | ubthlem.3 |
. . . . . 6
⊢ 𝐷 = (IndMet‘𝑈) |
18 | | ubthlem.4 |
. . . . . 6
⊢ 𝐽 = (MetOpen‘𝐷) |
19 | | ubthlem.5 |
. . . . . 6
⊢ 𝑈 ∈ CBan |
20 | | ubthlem.6 |
. . . . . 6
⊢ 𝑊 ∈ NrmCVec |
21 | | ubthlem.7 |
. . . . . . 7
⊢ (𝜑 → 𝑇 ⊆ (𝑈 BLnOp 𝑊)) |
22 | 21 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑧 ∈ 𝑋 ∃𝑑 ∈ ℝ ∀𝑢 ∈ 𝑇 (𝑁‘(𝑢‘𝑧)) ≤ 𝑑) → 𝑇 ⊆ (𝑈 BLnOp 𝑊)) |
23 | | simpr 476 |
. . . . . . 7
⊢ ((𝜑 ∧ ∀𝑧 ∈ 𝑋 ∃𝑑 ∈ ℝ ∀𝑢 ∈ 𝑇 (𝑁‘(𝑢‘𝑧)) ≤ 𝑑) → ∀𝑧 ∈ 𝑋 ∃𝑑 ∈ ℝ ∀𝑢 ∈ 𝑇 (𝑁‘(𝑢‘𝑧)) ≤ 𝑑) |
24 | 23, 14 | sylib 207 |
. . . . . 6
⊢ ((𝜑 ∧ ∀𝑧 ∈ 𝑋 ∃𝑑 ∈ ℝ ∀𝑢 ∈ 𝑇 (𝑁‘(𝑢‘𝑧)) ≤ 𝑑) → ∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐) |
25 | | fveq1 6102 |
. . . . . . . . . . . . 13
⊢ (𝑢 = 𝑡 → (𝑢‘𝑑) = (𝑡‘𝑑)) |
26 | 25 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑢 = 𝑡 → (𝑁‘(𝑢‘𝑑)) = (𝑁‘(𝑡‘𝑑))) |
27 | 26 | breq1d 4593 |
. . . . . . . . . . 11
⊢ (𝑢 = 𝑡 → ((𝑁‘(𝑢‘𝑑)) ≤ 𝑚 ↔ (𝑁‘(𝑡‘𝑑)) ≤ 𝑚)) |
28 | 27 | cbvralv 3147 |
. . . . . . . . . 10
⊢
(∀𝑢 ∈
𝑇 (𝑁‘(𝑢‘𝑑)) ≤ 𝑚 ↔ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑑)) ≤ 𝑚) |
29 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑑 = 𝑧 → (𝑡‘𝑑) = (𝑡‘𝑧)) |
30 | 29 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑑 = 𝑧 → (𝑁‘(𝑡‘𝑑)) = (𝑁‘(𝑡‘𝑧))) |
31 | 30 | breq1d 4593 |
. . . . . . . . . . 11
⊢ (𝑑 = 𝑧 → ((𝑁‘(𝑡‘𝑑)) ≤ 𝑚 ↔ (𝑁‘(𝑡‘𝑧)) ≤ 𝑚)) |
32 | 31 | ralbidv 2969 |
. . . . . . . . . 10
⊢ (𝑑 = 𝑧 → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑑)) ≤ 𝑚 ↔ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑚)) |
33 | 28, 32 | syl5bb 271 |
. . . . . . . . 9
⊢ (𝑑 = 𝑧 → (∀𝑢 ∈ 𝑇 (𝑁‘(𝑢‘𝑑)) ≤ 𝑚 ↔ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑚)) |
34 | 33 | cbvrabv 3172 |
. . . . . . . 8
⊢ {𝑑 ∈ 𝑋 ∣ ∀𝑢 ∈ 𝑇 (𝑁‘(𝑢‘𝑑)) ≤ 𝑚} = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑚} |
35 | | breq2 4587 |
. . . . . . . . . 10
⊢ (𝑚 = 𝑘 → ((𝑁‘(𝑡‘𝑧)) ≤ 𝑚 ↔ (𝑁‘(𝑡‘𝑧)) ≤ 𝑘)) |
36 | 35 | ralbidv 2969 |
. . . . . . . . 9
⊢ (𝑚 = 𝑘 → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑚 ↔ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘)) |
37 | 36 | rabbidv 3164 |
. . . . . . . 8
⊢ (𝑚 = 𝑘 → {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑚} = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘}) |
38 | 34, 37 | syl5eq 2656 |
. . . . . . 7
⊢ (𝑚 = 𝑘 → {𝑑 ∈ 𝑋 ∣ ∀𝑢 ∈ 𝑇 (𝑁‘(𝑢‘𝑑)) ≤ 𝑚} = {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘}) |
39 | 38 | cbvmptv 4678 |
. . . . . 6
⊢ (𝑚 ∈ ℕ ↦ {𝑑 ∈ 𝑋 ∣ ∀𝑢 ∈ 𝑇 (𝑁‘(𝑢‘𝑑)) ≤ 𝑚}) = (𝑘 ∈ ℕ ↦ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘}) |
40 | 15, 16, 17, 18, 19, 20, 22, 24, 39 | ubthlem1 27110 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑧 ∈ 𝑋 ∃𝑑 ∈ ℝ ∀𝑢 ∈ 𝑇 (𝑁‘(𝑢‘𝑧)) ≤ 𝑑) → ∃𝑛 ∈ ℕ ∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ ((𝑚 ∈ ℕ ↦ {𝑑 ∈ 𝑋 ∣ ∀𝑢 ∈ 𝑇 (𝑁‘(𝑢‘𝑑)) ≤ 𝑚})‘𝑛)) |
41 | 21 | ad3antrrr 762 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ∀𝑧 ∈ 𝑋 ∃𝑑 ∈ ℝ ∀𝑢 ∈ 𝑇 (𝑁‘(𝑢‘𝑧)) ≤ 𝑑) ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑋)) ∧ (𝑟 ∈ ℝ+ ∧ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ ((𝑚 ∈ ℕ ↦ {𝑑 ∈ 𝑋 ∣ ∀𝑢 ∈ 𝑇 (𝑁‘(𝑢‘𝑑)) ≤ 𝑚})‘𝑛))) → 𝑇 ⊆ (𝑈 BLnOp 𝑊)) |
42 | 24 | ad2antrr 758 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ∀𝑧 ∈ 𝑋 ∃𝑑 ∈ ℝ ∀𝑢 ∈ 𝑇 (𝑁‘(𝑢‘𝑧)) ≤ 𝑑) ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑋)) ∧ (𝑟 ∈ ℝ+ ∧ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ ((𝑚 ∈ ℕ ↦ {𝑑 ∈ 𝑋 ∣ ∀𝑢 ∈ 𝑇 (𝑁‘(𝑢‘𝑑)) ≤ 𝑚})‘𝑛))) → ∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐) |
43 | | simplrl 796 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ∀𝑧 ∈ 𝑋 ∃𝑑 ∈ ℝ ∀𝑢 ∈ 𝑇 (𝑁‘(𝑢‘𝑧)) ≤ 𝑑) ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑋)) ∧ (𝑟 ∈ ℝ+ ∧ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ ((𝑚 ∈ ℕ ↦ {𝑑 ∈ 𝑋 ∣ ∀𝑢 ∈ 𝑇 (𝑁‘(𝑢‘𝑑)) ≤ 𝑚})‘𝑛))) → 𝑛 ∈ ℕ) |
44 | | simplrr 797 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ∀𝑧 ∈ 𝑋 ∃𝑑 ∈ ℝ ∀𝑢 ∈ 𝑇 (𝑁‘(𝑢‘𝑧)) ≤ 𝑑) ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑋)) ∧ (𝑟 ∈ ℝ+ ∧ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ ((𝑚 ∈ ℕ ↦ {𝑑 ∈ 𝑋 ∣ ∀𝑢 ∈ 𝑇 (𝑁‘(𝑢‘𝑑)) ≤ 𝑚})‘𝑛))) → 𝑦 ∈ 𝑋) |
45 | | simprl 790 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ∀𝑧 ∈ 𝑋 ∃𝑑 ∈ ℝ ∀𝑢 ∈ 𝑇 (𝑁‘(𝑢‘𝑧)) ≤ 𝑑) ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑋)) ∧ (𝑟 ∈ ℝ+ ∧ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ ((𝑚 ∈ ℕ ↦ {𝑑 ∈ 𝑋 ∣ ∀𝑢 ∈ 𝑇 (𝑁‘(𝑢‘𝑑)) ≤ 𝑚})‘𝑛))) → 𝑟 ∈ ℝ+) |
46 | | simprr 792 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ ∀𝑧 ∈ 𝑋 ∃𝑑 ∈ ℝ ∀𝑢 ∈ 𝑇 (𝑁‘(𝑢‘𝑧)) ≤ 𝑑) ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑋)) ∧ (𝑟 ∈ ℝ+ ∧ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ ((𝑚 ∈ ℕ ↦ {𝑑 ∈ 𝑋 ∣ ∀𝑢 ∈ 𝑇 (𝑁‘(𝑢‘𝑑)) ≤ 𝑚})‘𝑛))) → {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ ((𝑚 ∈ ℕ ↦ {𝑑 ∈ 𝑋 ∣ ∀𝑢 ∈ 𝑇 (𝑁‘(𝑢‘𝑑)) ≤ 𝑚})‘𝑛)) |
47 | 15, 16, 17, 18, 19, 20, 41, 42, 39, 43, 44, 45, 46 | ubthlem2 27111 |
. . . . . . . 8
⊢ ((((𝜑 ∧ ∀𝑧 ∈ 𝑋 ∃𝑑 ∈ ℝ ∀𝑢 ∈ 𝑇 (𝑁‘(𝑢‘𝑧)) ≤ 𝑑) ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑋)) ∧ (𝑟 ∈ ℝ+ ∧ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ ((𝑚 ∈ ℕ ↦ {𝑑 ∈ 𝑋 ∣ ∀𝑢 ∈ 𝑇 (𝑁‘(𝑢‘𝑑)) ≤ 𝑚})‘𝑛))) → ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑) |
48 | 47 | expr 641 |
. . . . . . 7
⊢ ((((𝜑 ∧ ∀𝑧 ∈ 𝑋 ∃𝑑 ∈ ℝ ∀𝑢 ∈ 𝑇 (𝑁‘(𝑢‘𝑧)) ≤ 𝑑) ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑋)) ∧ 𝑟 ∈ ℝ+) → ({𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ ((𝑚 ∈ ℕ ↦ {𝑑 ∈ 𝑋 ∣ ∀𝑢 ∈ 𝑇 (𝑁‘(𝑢‘𝑑)) ≤ 𝑚})‘𝑛) → ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑)) |
49 | 48 | rexlimdva 3013 |
. . . . . 6
⊢ (((𝜑 ∧ ∀𝑧 ∈ 𝑋 ∃𝑑 ∈ ℝ ∀𝑢 ∈ 𝑇 (𝑁‘(𝑢‘𝑧)) ≤ 𝑑) ∧ (𝑛 ∈ ℕ ∧ 𝑦 ∈ 𝑋)) → (∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ ((𝑚 ∈ ℕ ↦ {𝑑 ∈ 𝑋 ∣ ∀𝑢 ∈ 𝑇 (𝑁‘(𝑢‘𝑑)) ≤ 𝑚})‘𝑛) → ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑)) |
50 | 49 | rexlimdvva 3020 |
. . . . 5
⊢ ((𝜑 ∧ ∀𝑧 ∈ 𝑋 ∃𝑑 ∈ ℝ ∀𝑢 ∈ 𝑇 (𝑁‘(𝑢‘𝑧)) ≤ 𝑑) → (∃𝑛 ∈ ℕ ∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ ((𝑚 ∈ ℕ ↦ {𝑑 ∈ 𝑋 ∣ ∀𝑢 ∈ 𝑇 (𝑁‘(𝑢‘𝑑)) ≤ 𝑚})‘𝑛) → ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑)) |
51 | 40, 50 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ ∀𝑧 ∈ 𝑋 ∃𝑑 ∈ ℝ ∀𝑢 ∈ 𝑇 (𝑁‘(𝑢‘𝑧)) ≤ 𝑑) → ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑) |
52 | 51 | ex 449 |
. . 3
⊢ (𝜑 → (∀𝑧 ∈ 𝑋 ∃𝑑 ∈ ℝ ∀𝑢 ∈ 𝑇 (𝑁‘(𝑢‘𝑧)) ≤ 𝑑 → ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑)) |
53 | 14, 52 | syl5bir 232 |
. 2
⊢ (𝜑 → (∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 → ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑)) |
54 | | simpr 476 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑑 ∈ ℝ) → 𝑑 ∈ ℝ) |
55 | | bnnv 27106 |
. . . . . . . 8
⊢ (𝑈 ∈ CBan → 𝑈 ∈
NrmCVec) |
56 | 19, 55 | ax-mp 5 |
. . . . . . 7
⊢ 𝑈 ∈ NrmCVec |
57 | | eqid 2610 |
. . . . . . . 8
⊢
(normCV‘𝑈) = (normCV‘𝑈) |
58 | 15, 57 | nvcl 26900 |
. . . . . . 7
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋) → ((normCV‘𝑈)‘𝑥) ∈ ℝ) |
59 | 56, 58 | mpan 702 |
. . . . . 6
⊢ (𝑥 ∈ 𝑋 → ((normCV‘𝑈)‘𝑥) ∈ ℝ) |
60 | | remulcl 9900 |
. . . . . 6
⊢ ((𝑑 ∈ ℝ ∧
((normCV‘𝑈)‘𝑥) ∈ ℝ) → (𝑑 · ((normCV‘𝑈)‘𝑥)) ∈ ℝ) |
61 | 54, 59, 60 | syl2an 493 |
. . . . 5
⊢ (((𝜑 ∧ 𝑑 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) → (𝑑 · ((normCV‘𝑈)‘𝑥)) ∈ ℝ) |
62 | 21 | sselda 3568 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ (𝑈 BLnOp 𝑊)) |
63 | 62 | adantlr 747 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑑 ∈ ℝ) ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ (𝑈 BLnOp 𝑊)) |
64 | 63 | ad2ant2r 779 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑑 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) ∧ (𝑡 ∈ 𝑇 ∧ ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑)) → 𝑡 ∈ (𝑈 BLnOp 𝑊)) |
65 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(BaseSet‘𝑊) =
(BaseSet‘𝑊) |
66 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑈 BLnOp 𝑊) = (𝑈 BLnOp 𝑊) |
67 | 15, 65, 66 | blof 27024 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑡 ∈ (𝑈 BLnOp 𝑊)) → 𝑡:𝑋⟶(BaseSet‘𝑊)) |
68 | 56, 20, 67 | mp3an12 1406 |
. . . . . . . . . . 11
⊢ (𝑡 ∈ (𝑈 BLnOp 𝑊) → 𝑡:𝑋⟶(BaseSet‘𝑊)) |
69 | 64, 68 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑑 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) ∧ (𝑡 ∈ 𝑇 ∧ ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑)) → 𝑡:𝑋⟶(BaseSet‘𝑊)) |
70 | | simplr 788 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑑 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) ∧ (𝑡 ∈ 𝑇 ∧ ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑)) → 𝑥 ∈ 𝑋) |
71 | 69, 70 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑑 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) ∧ (𝑡 ∈ 𝑇 ∧ ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑)) → (𝑡‘𝑥) ∈ (BaseSet‘𝑊)) |
72 | 65, 16 | nvcl 26900 |
. . . . . . . . . 10
⊢ ((𝑊 ∈ NrmCVec ∧ (𝑡‘𝑥) ∈ (BaseSet‘𝑊)) → (𝑁‘(𝑡‘𝑥)) ∈ ℝ) |
73 | 20, 72 | mpan 702 |
. . . . . . . . 9
⊢ ((𝑡‘𝑥) ∈ (BaseSet‘𝑊) → (𝑁‘(𝑡‘𝑥)) ∈ ℝ) |
74 | 71, 73 | syl 17 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑑 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) ∧ (𝑡 ∈ 𝑇 ∧ ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑)) → (𝑁‘(𝑡‘𝑥)) ∈ ℝ) |
75 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢ (𝑈 normOpOLD 𝑊) = (𝑈 normOpOLD 𝑊) |
76 | 15, 65, 75 | nmoxr 27005 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑡:𝑋⟶(BaseSet‘𝑊)) → ((𝑈 normOpOLD 𝑊)‘𝑡) ∈
ℝ*) |
77 | 56, 20, 76 | mp3an12 1406 |
. . . . . . . . . . 11
⊢ (𝑡:𝑋⟶(BaseSet‘𝑊) → ((𝑈 normOpOLD 𝑊)‘𝑡) ∈
ℝ*) |
78 | 69, 77 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑑 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) ∧ (𝑡 ∈ 𝑇 ∧ ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑)) → ((𝑈 normOpOLD 𝑊)‘𝑡) ∈
ℝ*) |
79 | | simpllr 795 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑑 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) ∧ (𝑡 ∈ 𝑇 ∧ ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑)) → 𝑑 ∈ ℝ) |
80 | 15, 65, 75 | nmogtmnf 27009 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑡:𝑋⟶(BaseSet‘𝑊)) → -∞ < ((𝑈 normOpOLD 𝑊)‘𝑡)) |
81 | 56, 20, 80 | mp3an12 1406 |
. . . . . . . . . . 11
⊢ (𝑡:𝑋⟶(BaseSet‘𝑊) → -∞ < ((𝑈 normOpOLD 𝑊)‘𝑡)) |
82 | 69, 81 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑑 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) ∧ (𝑡 ∈ 𝑇 ∧ ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑)) → -∞ < ((𝑈 normOpOLD 𝑊)‘𝑡)) |
83 | | simprr 792 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑑 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) ∧ (𝑡 ∈ 𝑇 ∧ ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑)) → ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑) |
84 | | xrre 11874 |
. . . . . . . . . 10
⊢
(((((𝑈
normOpOLD 𝑊)‘𝑡) ∈ ℝ* ∧ 𝑑 ∈ ℝ) ∧ (-∞
< ((𝑈
normOpOLD 𝑊)‘𝑡) ∧ ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑)) → ((𝑈 normOpOLD 𝑊)‘𝑡) ∈ ℝ) |
85 | 78, 79, 82, 83, 84 | syl22anc 1319 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑑 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) ∧ (𝑡 ∈ 𝑇 ∧ ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑)) → ((𝑈 normOpOLD 𝑊)‘𝑡) ∈ ℝ) |
86 | 59 | ad2antlr 759 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑑 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) ∧ (𝑡 ∈ 𝑇 ∧ ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑)) → ((normCV‘𝑈)‘𝑥) ∈ ℝ) |
87 | | remulcl 9900 |
. . . . . . . . 9
⊢ ((((𝑈 normOpOLD 𝑊)‘𝑡) ∈ ℝ ∧
((normCV‘𝑈)‘𝑥) ∈ ℝ) → (((𝑈 normOpOLD 𝑊)‘𝑡) · ((normCV‘𝑈)‘𝑥)) ∈ ℝ) |
88 | 85, 86, 87 | syl2anc 691 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑑 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) ∧ (𝑡 ∈ 𝑇 ∧ ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑)) → (((𝑈 normOpOLD 𝑊)‘𝑡) · ((normCV‘𝑈)‘𝑥)) ∈ ℝ) |
89 | 61 | adantr 480 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑑 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) ∧ (𝑡 ∈ 𝑇 ∧ ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑)) → (𝑑 · ((normCV‘𝑈)‘𝑥)) ∈ ℝ) |
90 | 15, 57, 16, 75, 66, 56, 20 | nmblolbi 27039 |
. . . . . . . . 9
⊢ ((𝑡 ∈ (𝑈 BLnOp 𝑊) ∧ 𝑥 ∈ 𝑋) → (𝑁‘(𝑡‘𝑥)) ≤ (((𝑈 normOpOLD 𝑊)‘𝑡) · ((normCV‘𝑈)‘𝑥))) |
91 | 64, 70, 90 | syl2anc 691 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑑 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) ∧ (𝑡 ∈ 𝑇 ∧ ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑)) → (𝑁‘(𝑡‘𝑥)) ≤ (((𝑈 normOpOLD 𝑊)‘𝑡) · ((normCV‘𝑈)‘𝑥))) |
92 | 15, 57 | nvge0 26912 |
. . . . . . . . . . . 12
⊢ ((𝑈 ∈ NrmCVec ∧ 𝑥 ∈ 𝑋) → 0 ≤
((normCV‘𝑈)‘𝑥)) |
93 | 56, 92 | mpan 702 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ 𝑋 → 0 ≤
((normCV‘𝑈)‘𝑥)) |
94 | 59, 93 | jca 553 |
. . . . . . . . . 10
⊢ (𝑥 ∈ 𝑋 → (((normCV‘𝑈)‘𝑥) ∈ ℝ ∧ 0 ≤
((normCV‘𝑈)‘𝑥))) |
95 | 94 | ad2antlr 759 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑑 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) ∧ (𝑡 ∈ 𝑇 ∧ ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑)) → (((normCV‘𝑈)‘𝑥) ∈ ℝ ∧ 0 ≤
((normCV‘𝑈)‘𝑥))) |
96 | | lemul1a 10756 |
. . . . . . . . 9
⊢
(((((𝑈
normOpOLD 𝑊)‘𝑡) ∈ ℝ ∧ 𝑑 ∈ ℝ ∧
(((normCV‘𝑈)‘𝑥) ∈ ℝ ∧ 0 ≤
((normCV‘𝑈)‘𝑥))) ∧ ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑) → (((𝑈 normOpOLD 𝑊)‘𝑡) · ((normCV‘𝑈)‘𝑥)) ≤ (𝑑 · ((normCV‘𝑈)‘𝑥))) |
97 | 85, 79, 95, 83, 96 | syl31anc 1321 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑑 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) ∧ (𝑡 ∈ 𝑇 ∧ ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑)) → (((𝑈 normOpOLD 𝑊)‘𝑡) · ((normCV‘𝑈)‘𝑥)) ≤ (𝑑 · ((normCV‘𝑈)‘𝑥))) |
98 | 74, 88, 89, 91, 97 | letrd 10073 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑑 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) ∧ (𝑡 ∈ 𝑇 ∧ ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑)) → (𝑁‘(𝑡‘𝑥)) ≤ (𝑑 · ((normCV‘𝑈)‘𝑥))) |
99 | 98 | expr 641 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑑 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) ∧ 𝑡 ∈ 𝑇) → (((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑 → (𝑁‘(𝑡‘𝑥)) ≤ (𝑑 · ((normCV‘𝑈)‘𝑥)))) |
100 | 99 | ralimdva 2945 |
. . . . 5
⊢ (((𝜑 ∧ 𝑑 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) → (∀𝑡 ∈ 𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑 → ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ (𝑑 · ((normCV‘𝑈)‘𝑥)))) |
101 | | breq2 4587 |
. . . . . . 7
⊢ (𝑐 = (𝑑 · ((normCV‘𝑈)‘𝑥)) → ((𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ↔ (𝑁‘(𝑡‘𝑥)) ≤ (𝑑 · ((normCV‘𝑈)‘𝑥)))) |
102 | 101 | ralbidv 2969 |
. . . . . 6
⊢ (𝑐 = (𝑑 · ((normCV‘𝑈)‘𝑥)) → (∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ↔ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ (𝑑 · ((normCV‘𝑈)‘𝑥)))) |
103 | 102 | rspcev 3282 |
. . . . 5
⊢ (((𝑑 ·
((normCV‘𝑈)‘𝑥)) ∈ ℝ ∧ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ (𝑑 · ((normCV‘𝑈)‘𝑥))) → ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐) |
104 | 61, 100, 103 | syl6an 566 |
. . . 4
⊢ (((𝜑 ∧ 𝑑 ∈ ℝ) ∧ 𝑥 ∈ 𝑋) → (∀𝑡 ∈ 𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑 → ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐)) |
105 | 104 | ralrimdva 2952 |
. . 3
⊢ ((𝜑 ∧ 𝑑 ∈ ℝ) → (∀𝑡 ∈ 𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑 → ∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐)) |
106 | 105 | rexlimdva 3013 |
. 2
⊢ (𝜑 → (∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑 → ∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐)) |
107 | 53, 106 | impbid 201 |
1
⊢ (𝜑 → (∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ↔ ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑)) |