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 4101 |
. . . . 5
⊢ (𝑇 ∩ 𝑆) = (𝑆 ∩ 𝑇) |
7 | | metnrmlem.4 |
. . . . 5
⊢ (𝜑 → (𝑆 ∩ 𝑇) = ∅) |
8 | 6, 7 | syl5eq 2786 |
. . . 4
⊢ (𝜑 → (𝑇 ∩ 𝑆) = ∅) |
9 | | metnrmlem.v |
. . . 4
⊢ 𝑉 = ∪ 𝑠 ∈ 𝑆 (𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) |
10 | 1, 2, 3, 4, 5, 8, 9 | metnrmlem2 23624 |
. . 3
⊢ (𝜑 → (𝑉 ∈ 𝐽 ∧ 𝑆 ⊆ 𝑉)) |
11 | 10 | simpld 498 |
. 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 23624 |
. . 3
⊢ (𝜑 → (𝑈 ∈ 𝐽 ∧ 𝑇 ⊆ 𝑈)) |
15 | 14 | simpld 498 |
. 2
⊢ (𝜑 → 𝑈 ∈ 𝐽) |
16 | 10 | simprd 499 |
. 2
⊢ (𝜑 → 𝑆 ⊆ 𝑉) |
17 | 14 | simprd 499 |
. 2
⊢ (𝜑 → 𝑇 ⊆ 𝑈) |
18 | 9 | ineq1i 4109 |
. . . 4
⊢ (𝑉 ∩ 𝑈) = (∪
𝑠 ∈ 𝑆 (𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ 𝑈) |
19 | | iunin1 4967 |
. . . 4
⊢ ∪ 𝑠 ∈ 𝑆 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ 𝑈) = (∪
𝑠 ∈ 𝑆 (𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ 𝑈) |
20 | 18, 19 | eqtr4i 2765 |
. . 3
⊢ (𝑉 ∩ 𝑈) = ∪
𝑠 ∈ 𝑆 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ 𝑈) |
21 | 13 | ineq2i 4110 |
. . . . . . . 8
⊢ ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ 𝑈) = ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ ∪ 𝑡 ∈ 𝑇 (𝑡(ball‘𝐷)(if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2))) |
22 | | iunin2 4966 |
. . . . . . . 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 2765 |
. . . . . . 7
⊢ ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ 𝑈) = ∪
𝑡 ∈ 𝑇 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ (𝑡(ball‘𝐷)(if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2))) |
24 | 3 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → 𝐷 ∈ (∞Met‘𝑋)) |
25 | | eqid 2739 |
. . . . . . . . . . . . . . . . 17
⊢ ∪ 𝐽 =
∪ 𝐽 |
26 | 25 | cldss 21792 |
. . . . . . . . . . . . . . . 16
⊢ (𝑆 ∈ (Clsd‘𝐽) → 𝑆 ⊆ ∪ 𝐽) |
27 | 5, 26 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑆 ⊆ ∪ 𝐽) |
28 | 2 | mopnuni 23206 |
. . . . . . . . . . . . . . . 16
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = ∪ 𝐽) |
29 | 3, 28 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑋 = ∪ 𝐽) |
30 | 27, 29 | sseqtrrd 3928 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑆 ⊆ 𝑋) |
31 | 30 | sselda 3887 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → 𝑠 ∈ 𝑋) |
32 | 31 | adantrr 717 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → 𝑠 ∈ 𝑋) |
33 | 25 | cldss 21792 |
. . . . . . . . . . . . . . . 16
⊢ (𝑇 ∈ (Clsd‘𝐽) → 𝑇 ⊆ ∪ 𝐽) |
34 | 4, 33 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑇 ⊆ ∪ 𝐽) |
35 | 34, 29 | sseqtrrd 3928 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝑇 ⊆ 𝑋) |
36 | 35 | sselda 3887 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → 𝑡 ∈ 𝑋) |
37 | 36 | adantrl 716 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → 𝑡 ∈ 𝑋) |
38 | 1, 2, 3, 4, 5, 8 | metnrmlem1a 23622 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → (0 < (𝐺‘𝑠) ∧ if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) ∈
ℝ+)) |
39 | 38 | simprd 499 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) ∈
ℝ+) |
40 | 39 | adantrr 717 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) ∈
ℝ+) |
41 | 40 | rphalfcld 12538 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2) ∈
ℝ+) |
42 | 41 | rpxrd 12527 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2) ∈
ℝ*) |
43 | 12, 2, 3, 5, 4, 7 | metnrmlem1a 23622 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑡 ∈ 𝑇) → (0 < (𝐹‘𝑡) ∧ if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) ∈
ℝ+)) |
44 | 43 | adantrl 716 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (0 < (𝐹‘𝑡) ∧ if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) ∈
ℝ+)) |
45 | 44 | simprd 499 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) ∈
ℝ+) |
46 | 45 | rphalfcld 12538 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2) ∈
ℝ+) |
47 | 46 | rpxrd 12527 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2) ∈
ℝ*) |
48 | 40 | rpred 12526 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) ∈ ℝ) |
49 | 48 | rehalfcld 11975 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2) ∈ ℝ) |
50 | 45 | rpred 12526 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) ∈ ℝ) |
51 | 50 | rehalfcld 11975 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2) ∈ ℝ) |
52 | 49, 51 | rexaddd 12722 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → ((if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2) +𝑒 (if(1 ≤
(𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2)) = ((if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2) + (if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2))) |
53 | 48 | recnd 10759 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) ∈ ℂ) |
54 | 50 | recnd 10759 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) ∈ ℂ) |
55 | | 2cnd 11806 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → 2 ∈ ℂ) |
56 | | 2ne0 11832 |
. . . . . . . . . . . . . . . 16
⊢ 2 ≠
0 |
57 | 56 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → 2 ≠ 0) |
58 | 53, 54, 55, 57 | divdird 11544 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → ((if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) / 2) = ((if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2) + (if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2))) |
59 | 52, 58 | eqtr4d 2777 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → ((if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2) +𝑒 (if(1 ≤
(𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2)) = ((if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) / 2)) |
60 | 1, 2, 3, 4, 5, 8 | metnrmlem1 23623 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑡 ∈ 𝑇 ∧ 𝑠 ∈ 𝑆)) → if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) ≤ (𝑡𝐷𝑠)) |
61 | 60 | ancom2s 650 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) ≤ (𝑡𝐷𝑠)) |
62 | | xmetsym 23112 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑡 ∈ 𝑋 ∧ 𝑠 ∈ 𝑋) → (𝑡𝐷𝑠) = (𝑠𝐷𝑡)) |
63 | 24, 37, 32, 62 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (𝑡𝐷𝑠) = (𝑠𝐷𝑡)) |
64 | 61, 63 | breqtrd 5066 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) ≤ (𝑠𝐷𝑡)) |
65 | 12, 2, 3, 5, 4, 7 | metnrmlem1 23623 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) ≤ (𝑠𝐷𝑡)) |
66 | 40 | rpxrd 12527 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) ∈
ℝ*) |
67 | 45 | rpxrd 12527 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) ∈
ℝ*) |
68 | | xmetcl 23096 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑠 ∈ 𝑋 ∧ 𝑡 ∈ 𝑋) → (𝑠𝐷𝑡) ∈
ℝ*) |
69 | 24, 32, 37, 68 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (𝑠𝐷𝑡) ∈
ℝ*) |
70 | | xle2add 12747 |
. . . . . . . . . . . . . . . . 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 838 |
. . . . . . . . . . . . . . . 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 10760 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) ∈ ℝ) |
74 | 73 | recnd 10759 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) ∈ ℂ) |
75 | 74, 55, 57 | divcan2d 11508 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (2 · ((if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) / 2)) = (if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)))) |
76 | | 2re 11802 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℝ |
77 | 73 | rehalfcld 11975 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → ((if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) / 2) ∈ ℝ) |
78 | | rexmul 12759 |
. . . . . . . . . . . . . . . . 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 590 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (2 ·e ((if(1
≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) / 2)) = (2 · ((if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) / 2))) |
80 | 48, 50 | rexaddd 12722 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) +𝑒 if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) = (if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)))) |
81 | 75, 79, 80 | 3eqtr4d 2784 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (2 ·e ((if(1
≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) / 2)) = (if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) +𝑒 if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)))) |
82 | | x2times 12787 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑠𝐷𝑡) ∈ ℝ* → (2
·e (𝑠𝐷𝑡)) = ((𝑠𝐷𝑡) +𝑒 (𝑠𝐷𝑡))) |
83 | 69, 82 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (2 ·e (𝑠𝐷𝑡)) = ((𝑠𝐷𝑡) +𝑒 (𝑠𝐷𝑡))) |
84 | 72, 81, 83 | 3brtr4d 5072 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (2 ·e ((if(1
≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) / 2)) ≤ (2 ·e (𝑠𝐷𝑡))) |
85 | 77 | rexrd 10781 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → ((if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) / 2) ∈
ℝ*) |
86 | | 2rp 12489 |
. . . . . . . . . . . . . . . 16
⊢ 2 ∈
ℝ+ |
87 | 86 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → 2 ∈
ℝ+) |
88 | | xlemul2 12779 |
. . . . . . . . . . . . . . 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 1372 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → (((if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) / 2) ≤ (𝑠𝐷𝑡) ↔ (2 ·e ((if(1 ≤
(𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) / 2)) ≤ (2 ·e (𝑠𝐷𝑡)))) |
90 | 84, 89 | mpbird 260 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → ((if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) + if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡))) / 2) ≤ (𝑠𝐷𝑡)) |
91 | 59, 90 | eqbrtrd 5062 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → ((if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2) +𝑒 (if(1 ≤
(𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2)) ≤ (𝑠𝐷𝑡)) |
92 | | bldisj 23163 |
. . . . . . . . . . . 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 1386 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑠 ∈ 𝑆 ∧ 𝑡 ∈ 𝑇)) → ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ (𝑡(ball‘𝐷)(if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2))) = ∅) |
94 | | eqimss 3943 |
. . . . . . . . . . 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 471 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑠 ∈ 𝑆) ∧ 𝑡 ∈ 𝑇) → ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ (𝑡(ball‘𝐷)(if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2))) ⊆ ∅) |
97 | 96 | ralrimiva 3097 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → ∀𝑡 ∈ 𝑇 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ (𝑡(ball‘𝐷)(if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2))) ⊆ ∅) |
98 | | iunss 4941 |
. . . . . . . 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 237 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → ∪
𝑡 ∈ 𝑇 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ (𝑡(ball‘𝐷)(if(1 ≤ (𝐹‘𝑡), 1, (𝐹‘𝑡)) / 2))) ⊆ ∅) |
100 | 23, 99 | eqsstrid 3935 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑠 ∈ 𝑆) → ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ 𝑈) ⊆ ∅) |
101 | 100 | ralrimiva 3097 |
. . . . 5
⊢ (𝜑 → ∀𝑠 ∈ 𝑆 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ 𝑈) ⊆ ∅) |
102 | | iunss 4941 |
. . . . 5
⊢ (∪ 𝑠 ∈ 𝑆 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ 𝑈) ⊆ ∅ ↔ ∀𝑠 ∈ 𝑆 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ 𝑈) ⊆ ∅) |
103 | 101, 102 | sylibr 237 |
. . . 4
⊢ (𝜑 → ∪ 𝑠 ∈ 𝑆 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺‘𝑠), 1, (𝐺‘𝑠)) / 2)) ∩ 𝑈) ⊆ ∅) |
104 | | ss0 4297 |
. . . 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 | syl5eq 2786 |
. 2
⊢ (𝜑 → (𝑉 ∩ 𝑈) = ∅) |
107 | | sseq2 3913 |
. . . 4
⊢ (𝑧 = 𝑉 → (𝑆 ⊆ 𝑧 ↔ 𝑆 ⊆ 𝑉)) |
108 | | ineq1 4106 |
. . . . 5
⊢ (𝑧 = 𝑉 → (𝑧 ∩ 𝑤) = (𝑉 ∩ 𝑤)) |
109 | 108 | eqeq1d 2741 |
. . . 4
⊢ (𝑧 = 𝑉 → ((𝑧 ∩ 𝑤) = ∅ ↔ (𝑉 ∩ 𝑤) = ∅)) |
110 | 107, 109 | 3anbi13d 1439 |
. . 3
⊢ (𝑧 = 𝑉 → ((𝑆 ⊆ 𝑧 ∧ 𝑇 ⊆ 𝑤 ∧ (𝑧 ∩ 𝑤) = ∅) ↔ (𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑤 ∧ (𝑉 ∩ 𝑤) = ∅))) |
111 | | sseq2 3913 |
. . . 4
⊢ (𝑤 = 𝑈 → (𝑇 ⊆ 𝑤 ↔ 𝑇 ⊆ 𝑈)) |
112 | | ineq2 4107 |
. . . . 5
⊢ (𝑤 = 𝑈 → (𝑉 ∩ 𝑤) = (𝑉 ∩ 𝑈)) |
113 | 112 | eqeq1d 2741 |
. . . 4
⊢ (𝑤 = 𝑈 → ((𝑉 ∩ 𝑤) = ∅ ↔ (𝑉 ∩ 𝑈) = ∅)) |
114 | 111, 113 | 3anbi23d 1440 |
. . 3
⊢ (𝑤 = 𝑈 → ((𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑤 ∧ (𝑉 ∩ 𝑤) = ∅) ↔ (𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑈 ∧ (𝑉 ∩ 𝑈) = ∅))) |
115 | 110, 114 | rspc2ev 3541 |
. 2
⊢ ((𝑉 ∈ 𝐽 ∧ 𝑈 ∈ 𝐽 ∧ (𝑆 ⊆ 𝑉 ∧ 𝑇 ⊆ 𝑈 ∧ (𝑉 ∩ 𝑈) = ∅)) → ∃𝑧 ∈ 𝐽 ∃𝑤 ∈ 𝐽 (𝑆 ⊆ 𝑧 ∧ 𝑇 ⊆ 𝑤 ∧ (𝑧 ∩ 𝑤) = ∅)) |
116 | 11, 15, 16, 17, 106, 115 | syl113anc 1383 |
1
⊢ (𝜑 → ∃𝑧 ∈ 𝐽 ∃𝑤 ∈ 𝐽 (𝑆 ⊆ 𝑧 ∧ 𝑇 ⊆ 𝑤 ∧ (𝑧 ∩ 𝑤) = ∅)) |