Proof of Theorem metnrmlem3
| Step | Hyp | Ref
| Expression |
| 1 | | metnrmlem.g |
. . . 4
⊢ 𝐺 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑇 ↦ (𝑥𝐷𝑦)), ℝ*, <
)) |
| 2 | | metdscn.j |
. . . 4
⊢ 𝐽 = (MetOpen‘𝐷) |
| 3 | | metnrmlem.1 |
. . . 4
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) |
| 4 | | metnrmlem.3 |
. . . 4
⊢ (𝜑 → 𝑇 ∈ (Clsd‘𝐽)) |
| 5 | | metnrmlem.2 |
. . . 4
⊢ (𝜑 → 𝑆 ∈ (Clsd‘𝐽)) |
| 6 | | incom 4209 |
. . . . 5
⊢ (𝑇 ∩ 𝑆) = (𝑆 ∩ 𝑇) |
| 7 | | metnrmlem.4 |
. . . . 5
⊢ (𝜑 → (𝑆 ∩ 𝑇) = ∅) |
| 8 | 6, 7 | eqtrid 2789 |
. . . 4
⊢ (𝜑 → (𝑇 ∩ 𝑆) = ∅) |
| 9 | | metnrmlem.v |
. . . 4
⊢ 𝑉 = ∪ 𝑠 ∈ 𝑆 (𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) |
| 10 | 1, 2, 3, 4, 5, 8, 9 | metnrmlem2 24882 |
. . 3
⊢ (𝜑 → (𝑉 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑉)) |
| 11 | 10 | simpld 494 |
. 2
⊢ (𝜑 → 𝑉 ∈ 𝐽) |
| 12 | | metdscn.f |
. . . 4
⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ inf(ran (𝑦 ∈ 𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, <
)) |
| 13 | | metnrmlem.u |
. . . 4
⊢ 𝑈 = ∪ 𝑡 ∈ 𝑇 (𝑡(ball‘𝐷)(if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2)) |
| 14 | 12, 2, 3, 5, 4, 7, 13 | metnrmlem2 24882 |
. . 3
⊢ (𝜑 → (𝑈 ∈ 𝐽 ∧ 𝑇 ⊆ 𝑈)) |
| 15 | 14 | simpld 494 |
. 2
⊢ (𝜑 → 𝑈 ∈ 𝐽) |
| 16 | 10 | simprd 495 |
. 2
⊢ (𝜑 → 𝑆 ⊆ 𝑉) |
| 17 | 14 | simprd 495 |
. 2
⊢ (𝜑 → 𝑇 ⊆ 𝑈) |
| 18 | 9 | ineq1i 4216 |
. . . 4
⊢ (𝑉 ∩ 𝑈) = (∪
𝑠 ∈ 𝑆 (𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ 𝑈) |
| 19 | | iunin1 5072 |
. . . 4
⊢ ∪ 𝑠 ∈ 𝑆 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ 𝑈) = (∪
𝑠 ∈ 𝑆 (𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ 𝑈) |
| 20 | 18, 19 | eqtr4i 2768 |
. . 3
⊢ (𝑉 ∩ 𝑈) = ∪
𝑠 ∈ 𝑆 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ 𝑈) |
| 21 | 13 | ineq2i 4217 |
. . . . . . . 8
⊢ ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ 𝑈) = ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ ∪ 𝑡 ∈ 𝑇 (𝑡(ball‘𝐷)(if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2))) |
| 22 | | iunin2 5071 |
. . . . . . . 8
⊢ ∪ 𝑡 ∈ 𝑇 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ (𝑡(ball‘𝐷)(if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2))) = ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ ∪ 𝑡 ∈ 𝑇 (𝑡(ball‘𝐷)(if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2))) |
| 23 | 21, 22 | eqtr4i 2768 |
. . . . . . 7
⊢ ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ 𝑈) = ∪
𝑡 ∈ 𝑇 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ (𝑡(ball‘𝐷)(if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2))) |
| 24 | 3 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → 𝐷 ∈ (∞Met‘𝑋)) |
| 25 | | eqid 2737 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ 𝐽 =
∪ 𝐽 |
| 26 | 25 | cldss 23037 |
. . . . . . . . . . . . . . . 16
⊢ (𝑆 ∈ (Clsd‘𝐽) → 𝑆 ⊆ ∪ 𝐽) |
| 27 | 5, 26 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑆 ⊆ ∪ 𝐽) |
| 28 | 2 | mopnuni 24451 |
. . . . . . . . . . . . . . . 16
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = ∪ 𝐽) |
| 29 | 3, 28 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑋 = ∪ 𝐽) |
| 30 | 27, 29 | sseqtrrd 4021 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ⊆ 𝑋) |
| 31 | 30 | sselda 3983 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ 𝑋) |
| 32 | 31 | adantrr 717 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → 𝑠 ∈ 𝑋) |
| 33 | 25 | cldss 23037 |
. . . . . . . . . . . . . . . 16
⊢ (𝑇 ∈ (Clsd‘𝐽) → 𝑇 ⊆ ∪ 𝐽) |
| 34 | 4, 33 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑇 ⊆ ∪ 𝐽) |
| 35 | 34, 29 | sseqtrrd 4021 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑇 ⊆ 𝑋) |
| 36 | 35 | sselda 3983 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ 𝑋) |
| 37 | 36 | adantrl 716 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → 𝑡 ∈ 𝑋) |
| 38 | 1, 2, 3, 4, 5, 8 | metnrmlem1a 24880 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (0 < (𝐺‘𝑠) ∧ if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) ∈
ℝ+)) |
| 39 | 38 | simprd 495 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) ∈
ℝ+) |
| 40 | 39 | adantrr 717 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) ∈
ℝ+) |
| 41 | 40 | rphalfcld 13089 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2) ∈
ℝ+) |
| 42 | 41 | rpxrd 13078 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2) ∈
ℝ*) |
| 43 | 12, 2, 3, 5, 4, 7 | metnrmlem1a 24880 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (0 < (𝐹‘𝑡) ∧ if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) ∈
ℝ+)) |
| 44 | 43 | adantrl 716 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (0 < (𝐹‘𝑡) ∧ if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) ∈
ℝ+)) |
| 45 | 44 | simprd 495 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) ∈
ℝ+) |
| 46 | 45 | rphalfcld 13089 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2) ∈
ℝ+) |
| 47 | 46 | rpxrd 13078 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2) ∈
ℝ*) |
| 48 | 40 | rpred 13077 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) ∈ ℝ) |
| 49 | 48 | rehalfcld 12513 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2) ∈ ℝ) |
| 50 | 45 | rpred 13077 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) ∈ ℝ) |
| 51 | 50 | rehalfcld 12513 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2) ∈ ℝ) |
| 52 | 49, 51 | rexaddd 13276 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → ((if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2) +𝑒 (if(1 ≤
(𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2)) = ((if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2) + (if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2))) |
| 53 | 48 | recnd 11289 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) ∈ ℂ) |
| 54 | 50 | recnd 11289 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) ∈ ℂ) |
| 55 | | 2cnd 12344 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → 2 ∈ ℂ) |
| 56 | | 2ne0 12370 |
. . . . . . . . . . . . . . . 16
⊢ 2 ≠
0 |
| 57 | 56 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → 2 ≠ 0) |
| 58 | 53, 54, 55, 57 | divdird 12081 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → ((if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) / 2) = ((if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2) + (if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2))) |
| 59 | 52, 58 | eqtr4d 2780 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → ((if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2) +𝑒 (if(1 ≤
(𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2)) = ((if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) / 2)) |
| 60 | 1, 2, 3, 4, 5, 8 | metnrmlem1 24881 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑇 ∧ 𝑠 ∈ 𝑆)) → if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) ≤ (𝑡𝐷𝑠)) |
| 61 | 60 | ancom2s 650 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) ≤ (𝑡𝐷𝑠)) |
| 62 | | xmetsym 24357 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑡 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋) → (𝑡𝐷𝑠) = (𝑠𝐷𝑡)) |
| 63 | 24, 37, 32, 62 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (𝑡𝐷𝑠) = (𝑠𝐷𝑡)) |
| 64 | 61, 63 | breqtrd 5169 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) ≤ (𝑠𝐷𝑡)) |
| 65 | 12, 2, 3, 5, 4, 7 | metnrmlem1 24881 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) ≤ (𝑠𝐷𝑡)) |
| 66 | 40 | rpxrd 13078 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) ∈
ℝ*) |
| 67 | 45 | rpxrd 13078 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) ∈
ℝ*) |
| 68 | | xmetcl 24341 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑠 ∈ 𝑋 ∧ 𝑡 ∈ 𝑋) → (𝑠𝐷𝑡) ∈
ℝ*) |
| 69 | 24, 32, 37, 68 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (𝑠𝐷𝑡) ∈
ℝ*) |
| 70 | | xle2add 13301 |
. . . . . . . . . . . . . . . . 17
⊢ (((if(1
≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) ∈ ℝ* ∧ if(1 ≤
(𝐹‘𝑡), 1, (𝐹‘𝑡)) ∈ ℝ*) ∧ ((𝑠𝐷𝑡) ∈ ℝ* ∧ (𝑠𝐷𝑡) ∈ ℝ*)) → ((if(1
≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) ≤ (𝑠𝐷𝑡) ∧ if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) ≤ (𝑠𝐷𝑡)) → (if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) +𝑒 if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) ≤ ((𝑠𝐷𝑡) +𝑒 (𝑠𝐷𝑡)))) |
| 71 | 66, 67, 69, 69, 70 | syl22anc 839 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → ((if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) ≤ (𝑠𝐷𝑡) ∧ if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) ≤ (𝑠𝐷𝑡)) → (if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) +𝑒 if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) ≤ ((𝑠𝐷𝑡) +𝑒 (𝑠𝐷𝑡)))) |
| 72 | 64, 65, 71 | mp2and 699 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) +𝑒 if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) ≤ ((𝑠𝐷𝑡) +𝑒 (𝑠𝐷𝑡))) |
| 73 | 48, 50 | readdcld 11290 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) ∈ ℝ) |
| 74 | 73 | recnd 11289 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) ∈ ℂ) |
| 75 | 74, 55, 57 | divcan2d 12045 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (2 · ((if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) / 2)) = (if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)))) |
| 76 | | 2re 12340 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℝ |
| 77 | 73 | rehalfcld 12513 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → ((if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) / 2) ∈ ℝ) |
| 78 | | rexmul 13313 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
∈ ℝ ∧ ((if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) / 2) ∈ ℝ) → (2
·e ((if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) / 2)) = (2 · ((if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) / 2))) |
| 79 | 76, 77, 78 | sylancr 587 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (2 ·e ((if(1
≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) / 2)) = (2 · ((if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) / 2))) |
| 80 | 48, 50 | rexaddd 13276 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) +𝑒 if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) = (if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)))) |
| 81 | 75, 79, 80 | 3eqtr4d 2787 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (2 ·e ((if(1
≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) / 2)) = (if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) +𝑒 if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)))) |
| 82 | | x2times 13341 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑠𝐷𝑡) ∈ ℝ* → (2
·e (𝑠𝐷𝑡)) = ((𝑠𝐷𝑡) +𝑒 (𝑠𝐷𝑡))) |
| 83 | 69, 82 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (2 ·e (𝑠𝐷𝑡)) = ((𝑠𝐷𝑡) +𝑒 (𝑠𝐷𝑡))) |
| 84 | 72, 81, 83 | 3brtr4d 5175 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (2 ·e ((if(1
≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) / 2)) ≤ (2 ·e (𝑠𝐷𝑡))) |
| 85 | 77 | rexrd 11311 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → ((if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) / 2) ∈
ℝ*) |
| 86 | | 2rp 13039 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℝ+ |
| 87 | 86 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → 2 ∈
ℝ+) |
| 88 | | xlemul2 13333 |
. . . . . . . . . . . . . . 15
⊢ ((((if(1
≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) / 2) ∈ ℝ* ∧
(𝑠𝐷𝑡) ∈ ℝ* ∧ 2 ∈
ℝ+) → (((if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) / 2) ≤ (𝑠𝐷𝑡) ↔ (2 ·e ((if(1 ≤
(𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) / 2)) ≤ (2 ·e (𝑠𝐷𝑡)))) |
| 89 | 85, 69, 87, 88 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (((if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) / 2) ≤ (𝑠𝐷𝑡) ↔ (2 ·e ((if(1 ≤
(𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) / 2)) ≤ (2 ·e (𝑠𝐷𝑡)))) |
| 90 | 84, 89 | mpbird 257 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → ((if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) / 2) ≤ (𝑠𝐷𝑡)) |
| 91 | 59, 90 | eqbrtrd 5165 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → ((if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2) +𝑒 (if(1 ≤
(𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2)) ≤ (𝑠𝐷𝑡)) |
| 92 | | bldisj 24408 |
. . . . . . . . . . . 12
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑠 ∈ 𝑋 ∧ 𝑡 ∈ 𝑋) ∧ ((if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2) ∈ ℝ* ∧
(if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2) ∈ ℝ* ∧
((if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2) +𝑒 (if(1 ≤
(𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2)) ≤ (𝑠𝐷𝑡))) → ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ (𝑡(ball‘𝐷)(if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2))) = ∅) |
| 93 | 24, 32, 37, 42, 47, 91, 92 | syl33anc 1387 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ (𝑡(ball‘𝐷)(if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2))) = ∅) |
| 94 | | eqimss 4042 |
. . . . . . . . . . 11
⊢ (((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ (𝑡(ball‘𝐷)(if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2))) = ∅ → ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ (𝑡(ball‘𝐷)(if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2))) ⊆ ∅) |
| 95 | 93, 94 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ (𝑡(ball‘𝐷)(if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2))) ⊆ ∅) |
| 96 | 95 | anassrs 467 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ 𝑆) ∧ 𝑡 ∈ 𝑇) → ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ (𝑡(ball‘𝐷)(if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2))) ⊆ ∅) |
| 97 | 96 | ralrimiva 3146 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → ∀𝑡 ∈ 𝑇 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ (𝑡(ball‘𝐷)(if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2))) ⊆ ∅) |
| 98 | | iunss 5045 |
. . . . . . . 8
⊢ (∪ 𝑡 ∈ 𝑇 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ (𝑡(ball‘𝐷)(if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2))) ⊆ ∅ ↔
∀𝑡 ∈ 𝑇 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ (𝑡(ball‘𝐷)(if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2))) ⊆ ∅) |
| 99 | 97, 98 | sylibr 234 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → ∪
𝑡 ∈ 𝑇 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ (𝑡(ball‘𝐷)(if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2))) ⊆ ∅) |
| 100 | 23, 99 | eqsstrid 4022 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ 𝑈) ⊆ ∅) |
| 101 | 100 | ralrimiva 3146 |
. . . . 5
⊢ (𝜑 → ∀𝑠 ∈ 𝑆 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ 𝑈) ⊆ ∅) |
| 102 | | iunss 5045 |
. . . . 5
⊢ (∪ 𝑠 ∈ 𝑆 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ 𝑈) ⊆ ∅ ↔ ∀𝑠 ∈ 𝑆 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ 𝑈) ⊆ ∅) |
| 103 | 101, 102 | sylibr 234 |
. . . 4
⊢ (𝜑 → ∪ 𝑠 ∈ 𝑆 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ 𝑈) ⊆ ∅) |
| 104 | | ss0 4402 |
. . . 4
⊢ (∪ 𝑠 ∈ 𝑆 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ 𝑈) ⊆ ∅ → ∪ 𝑠 ∈ 𝑆 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ 𝑈) = ∅) |
| 105 | 103, 104 | syl 17 |
. . 3
⊢ (𝜑 → ∪ 𝑠 ∈ 𝑆 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ 𝑈) = ∅) |
| 106 | 20, 105 | eqtrid 2789 |
. 2
⊢ (𝜑 → (𝑉 ∩ 𝑈) = ∅) |
| 107 | | sseq2 4010 |
. . . 4
⊢ (𝑧 = 𝑉 → (𝑆 ⊆ 𝑧 ↔ 𝑆 ⊆ 𝑉)) |
| 108 | | ineq1 4213 |
. . . . 5
⊢ (𝑧 = 𝑉 → (𝑧 ∩ 𝑤) = (𝑉 ∩ 𝑤)) |
| 109 | 108 | eqeq1d 2739 |
. . . 4
⊢ (𝑧 = 𝑉 → ((𝑧 ∩ 𝑤) = ∅ ↔ (𝑉 ∩ 𝑤) = ∅)) |
| 110 | 107, 109 | 3anbi13d 1440 |
. . 3
⊢ (𝑧 = 𝑉 → ((𝑆 ⊆ 𝑧 ∧ 𝑇 ⊆ 𝑤 ∧ (𝑧 ∩ 𝑤) = ∅) ↔ (𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑤 ∧ (𝑉 ∩ 𝑤) = ∅))) |
| 111 | | sseq2 4010 |
. . . 4
⊢ (𝑤 = 𝑈 → (𝑇 ⊆ 𝑤 ↔ 𝑇 ⊆ 𝑈)) |
| 112 | | ineq2 4214 |
. . . . 5
⊢ (𝑤 = 𝑈 → (𝑉 ∩ 𝑤) = (𝑉 ∩ 𝑈)) |
| 113 | 112 | eqeq1d 2739 |
. . . 4
⊢ (𝑤 = 𝑈 → ((𝑉 ∩ 𝑤) = ∅ ↔ (𝑉 ∩ 𝑈) = ∅)) |
| 114 | 111, 113 | 3anbi23d 1441 |
. . 3
⊢ (𝑤 = 𝑈 → ((𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑤 ∧ (𝑉 ∩ 𝑤) = ∅) ↔ (𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑈 ∧ (𝑉 ∩ 𝑈) = ∅))) |
| 115 | 110, 114 | rspc2ev 3635 |
. 2
⊢ ((𝑉 ∈ 𝐽 ∧ 𝑈 ∈ 𝐽 ∧ (𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑈 ∧ (𝑉 ∩ 𝑈) = ∅)) → ∃𝑧 ∈ 𝐽 ∃𝑤 ∈ 𝐽 (𝑆 ⊆ 𝑧 ∧ 𝑇 ⊆ 𝑤 ∧ (𝑧 ∩ 𝑤) = ∅)) |
| 116 | 11, 15, 16, 17, 106, 115 | syl113anc 1384 |
1
⊢ (𝜑 → ∃𝑧 ∈ 𝐽 ∃𝑤 ∈ 𝐽 (𝑆 ⊆ 𝑧 ∧ 𝑇 ⊆ 𝑤 ∧ (𝑧 ∩ 𝑤) = ∅)) |