MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  metnrmlem3 Structured version   Visualization version   GIF version

Theorem metnrmlem3 22711
Description: Lemma for metnrm 22712. (Contributed by Mario Carneiro, 14-Jan-2014.) (Revised by Mario Carneiro, 5-Sep-2015.)
Hypotheses
Ref Expression
metdscn.f 𝐹 = (𝑥𝑋 ↦ inf(ran (𝑦𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))
metdscn.j 𝐽 = (MetOpen‘𝐷)
metnrmlem.1 (𝜑𝐷 ∈ (∞Met‘𝑋))
metnrmlem.2 (𝜑𝑆 ∈ (Clsd‘𝐽))
metnrmlem.3 (𝜑𝑇 ∈ (Clsd‘𝐽))
metnrmlem.4 (𝜑 → (𝑆𝑇) = ∅)
metnrmlem.u 𝑈 = 𝑡𝑇 (𝑡(ball‘𝐷)(if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2))
metnrmlem.g 𝐺 = (𝑥𝑋 ↦ inf(ran (𝑦𝑇 ↦ (𝑥𝐷𝑦)), ℝ*, < ))
metnrmlem.v 𝑉 = 𝑠𝑆 (𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2))
Assertion
Ref Expression
metnrmlem3 (𝜑 → ∃𝑧𝐽𝑤𝐽 (𝑆𝑧𝑇𝑤 ∧ (𝑧𝑤) = ∅))
Distinct variable groups:   𝑥,𝑤,𝑦,𝑧   𝑡,𝑠,𝑤,𝑥,𝑦,𝑧,𝐷   𝐽,𝑠,𝑡,𝑤,𝑦,𝑧   𝜑,𝑠,𝑡   𝐺,𝑠,𝑡   𝑇,𝑠,𝑡,𝑤,𝑥,𝑦,𝑧   𝑆,𝑠,𝑡,𝑤,𝑥,𝑦,𝑧   𝑈,𝑠,𝑤   𝑋,𝑠,𝑡,𝑤,𝑥,𝑦,𝑧   𝐹,𝑠,𝑡,𝑤,𝑧   𝑤,𝑉,𝑧
Allowed substitution hints:   𝜑(𝑥,𝑦,𝑧,𝑤)   𝑈(𝑥,𝑦,𝑧,𝑡)   𝐹(𝑥,𝑦)   𝐺(𝑥,𝑦,𝑧,𝑤)   𝐽(𝑥)   𝑉(𝑥,𝑦,𝑡,𝑠)

Proof of Theorem metnrmlem3
StepHypRef 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 3838 . . . . 5 (𝑇𝑆) = (𝑆𝑇)
7 metnrmlem.4 . . . . 5 (𝜑 → (𝑆𝑇) = ∅)
86, 7syl5eq 2697 . . . 4 (𝜑 → (𝑇𝑆) = ∅)
9 metnrmlem.v . . . 4 𝑉 = 𝑠𝑆 (𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2))
101, 2, 3, 4, 5, 8, 9metnrmlem2 22710 . . 3 (𝜑 → (𝑉𝐽𝑆𝑉))
1110simpld 474 . 2 (𝜑𝑉𝐽)
12 metdscn.f . . . 4 𝐹 = (𝑥𝑋 ↦ inf(ran (𝑦𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))
13 metnrmlem.u . . . 4 𝑈 = 𝑡𝑇 (𝑡(ball‘𝐷)(if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2))
1412, 2, 3, 5, 4, 7, 13metnrmlem2 22710 . . 3 (𝜑 → (𝑈𝐽𝑇𝑈))
1514simpld 474 . 2 (𝜑𝑈𝐽)
1610simprd 478 . 2 (𝜑𝑆𝑉)
1714simprd 478 . 2 (𝜑𝑇𝑈)
189ineq1i 3843 . . . 4 (𝑉𝑈) = ( 𝑠𝑆 (𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ 𝑈)
19 iunin1 4617 . . . 4 𝑠𝑆 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ 𝑈) = ( 𝑠𝑆 (𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ 𝑈)
2018, 19eqtr4i 2676 . . 3 (𝑉𝑈) = 𝑠𝑆 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ 𝑈)
2113ineq2i 3844 . . . . . . . 8 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ 𝑈) = ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ 𝑡𝑇 (𝑡(ball‘𝐷)(if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2)))
22 iunin2 4616 . . . . . . . 8 𝑡𝑇 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ (𝑡(ball‘𝐷)(if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2))) = ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ 𝑡𝑇 (𝑡(ball‘𝐷)(if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2)))
2321, 22eqtr4i 2676 . . . . . . 7 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ 𝑈) = 𝑡𝑇 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ (𝑡(ball‘𝐷)(if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2)))
243adantr 480 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → 𝐷 ∈ (∞Met‘𝑋))
25 eqid 2651 . . . . . . . . . . . . . . . . 17 𝐽 = 𝐽
2625cldss 20881 . . . . . . . . . . . . . . . 16 (𝑆 ∈ (Clsd‘𝐽) → 𝑆 𝐽)
275, 26syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑆 𝐽)
282mopnuni 22293 . . . . . . . . . . . . . . . 16 (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = 𝐽)
293, 28syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑋 = 𝐽)
3027, 29sseqtr4d 3675 . . . . . . . . . . . . . 14 (𝜑𝑆𝑋)
3130sselda 3636 . . . . . . . . . . . . 13 ((𝜑𝑠𝑆) → 𝑠𝑋)
3231adantrr 753 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → 𝑠𝑋)
3325cldss 20881 . . . . . . . . . . . . . . . 16 (𝑇 ∈ (Clsd‘𝐽) → 𝑇 𝐽)
344, 33syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑇 𝐽)
3534, 29sseqtr4d 3675 . . . . . . . . . . . . . 14 (𝜑𝑇𝑋)
3635sselda 3636 . . . . . . . . . . . . 13 ((𝜑𝑡𝑇) → 𝑡𝑋)
3736adantrl 752 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → 𝑡𝑋)
381, 2, 3, 4, 5, 8metnrmlem1a 22708 . . . . . . . . . . . . . . . 16 ((𝜑𝑠𝑆) → (0 < (𝐺𝑠) ∧ if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) ∈ ℝ+))
3938simprd 478 . . . . . . . . . . . . . . 15 ((𝜑𝑠𝑆) → if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) ∈ ℝ+)
4039adantrr 753 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) ∈ ℝ+)
4140rphalfcld 11922 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2) ∈ ℝ+)
4241rpxrd 11911 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2) ∈ ℝ*)
4312, 2, 3, 5, 4, 7metnrmlem1a 22708 . . . . . . . . . . . . . . . 16 ((𝜑𝑡𝑇) → (0 < (𝐹𝑡) ∧ if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) ∈ ℝ+))
4443adantrl 752 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (0 < (𝐹𝑡) ∧ if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) ∈ ℝ+))
4544simprd 478 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) ∈ ℝ+)
4645rphalfcld 11922 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2) ∈ ℝ+)
4746rpxrd 11911 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2) ∈ ℝ*)
4840rpred 11910 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) ∈ ℝ)
4948rehalfcld 11317 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2) ∈ ℝ)
5045rpred 11910 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) ∈ ℝ)
5150rehalfcld 11317 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2) ∈ ℝ)
52 rexadd 12101 . . . . . . . . . . . . . . 15 (((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2) ∈ ℝ ∧ (if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2) ∈ ℝ) → ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2) +𝑒 (if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2)) = ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2) + (if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2)))
5349, 51, 52syl2anc 694 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2) +𝑒 (if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2)) = ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2) + (if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2)))
5448recnd 10106 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) ∈ ℂ)
5550recnd 10106 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) ∈ ℂ)
56 2cnd 11131 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → 2 ∈ ℂ)
57 2ne0 11151 . . . . . . . . . . . . . . . 16 2 ≠ 0
5857a1i 11 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → 2 ≠ 0)
5954, 55, 56, 58divdird 10877 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) + if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))) / 2) = ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2) + (if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2)))
6053, 59eqtr4d 2688 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2) +𝑒 (if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2)) = ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) + if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))) / 2))
611, 2, 3, 4, 5, 8metnrmlem1 22709 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡𝑇𝑠𝑆)) → if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) ≤ (𝑡𝐷𝑠))
6261ancom2s 861 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) ≤ (𝑡𝐷𝑠))
63 xmetsym 22199 . . . . . . . . . . . . . . . . . 18 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑡𝑋𝑠𝑋) → (𝑡𝐷𝑠) = (𝑠𝐷𝑡))
6424, 37, 32, 63syl3anc 1366 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (𝑡𝐷𝑠) = (𝑠𝐷𝑡))
6562, 64breqtrd 4711 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) ≤ (𝑠𝐷𝑡))
6612, 2, 3, 5, 4, 7metnrmlem1 22709 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) ≤ (𝑠𝐷𝑡))
6740rpxrd 11911 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) ∈ ℝ*)
6845rpxrd 11911 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) ∈ ℝ*)
69 xmetcl 22183 . . . . . . . . . . . . . . . . . 18 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑠𝑋𝑡𝑋) → (𝑠𝐷𝑡) ∈ ℝ*)
7024, 32, 37, 69syl3anc 1366 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (𝑠𝐷𝑡) ∈ ℝ*)
71 xle2add 12127 . . . . . . . . . . . . . . . . 17 (((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) ∈ ℝ* ∧ if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) ∈ ℝ*) ∧ ((𝑠𝐷𝑡) ∈ ℝ* ∧ (𝑠𝐷𝑡) ∈ ℝ*)) → ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) ≤ (𝑠𝐷𝑡) ∧ if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) ≤ (𝑠𝐷𝑡)) → (if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) +𝑒 if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))) ≤ ((𝑠𝐷𝑡) +𝑒 (𝑠𝐷𝑡))))
7267, 68, 70, 70, 71syl22anc 1367 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) ≤ (𝑠𝐷𝑡) ∧ if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) ≤ (𝑠𝐷𝑡)) → (if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) +𝑒 if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))) ≤ ((𝑠𝐷𝑡) +𝑒 (𝑠𝐷𝑡))))
7365, 66, 72mp2and 715 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) +𝑒 if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))) ≤ ((𝑠𝐷𝑡) +𝑒 (𝑠𝐷𝑡)))
7448, 50readdcld 10107 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) + if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))) ∈ ℝ)
7574recnd 10106 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) + if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))) ∈ ℂ)
7675, 56, 58divcan2d 10841 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (2 · ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) + if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))) / 2)) = (if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) + if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))))
77 2re 11128 . . . . . . . . . . . . . . . . 17 2 ∈ ℝ
7874rehalfcld 11317 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) + if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))) / 2) ∈ ℝ)
79 rexmul 12139 . . . . . . . . . . . . . . . . 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)))
8077, 78, 79sylancr 696 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (2 ·e ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) + if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))) / 2)) = (2 · ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) + if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))) / 2)))
81 rexadd 12101 . . . . . . . . . . . . . . . . 17 ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) ∈ ℝ ∧ if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) ∈ ℝ) → (if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) +𝑒 if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))) = (if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) + if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))))
8248, 50, 81syl2anc 694 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) +𝑒 if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))) = (if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) + if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))))
8376, 80, 823eqtr4d 2695 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (2 ·e ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) + if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))) / 2)) = (if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) +𝑒 if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))))
84 x2times 12167 . . . . . . . . . . . . . . . 16 ((𝑠𝐷𝑡) ∈ ℝ* → (2 ·e (𝑠𝐷𝑡)) = ((𝑠𝐷𝑡) +𝑒 (𝑠𝐷𝑡)))
8570, 84syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (2 ·e (𝑠𝐷𝑡)) = ((𝑠𝐷𝑡) +𝑒 (𝑠𝐷𝑡)))
8673, 83, 853brtr4d 4717 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (2 ·e ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) + if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))) / 2)) ≤ (2 ·e (𝑠𝐷𝑡)))
8778rexrd 10127 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) + if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))) / 2) ∈ ℝ*)
88 2rp 11875 . . . . . . . . . . . . . . . 16 2 ∈ ℝ+
8988a1i 11 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → 2 ∈ ℝ+)
90 xlemul2 12159 . . . . . . . . . . . . . . 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 (𝑠𝐷𝑡))))
9187, 70, 89, 90syl3anc 1366 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) + if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))) / 2) ≤ (𝑠𝐷𝑡) ↔ (2 ·e ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) + if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))) / 2)) ≤ (2 ·e (𝑠𝐷𝑡))))
9286, 91mpbird 247 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) + if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))) / 2) ≤ (𝑠𝐷𝑡))
9360, 92eqbrtrd 4707 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2) +𝑒 (if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2)) ≤ (𝑠𝐷𝑡))
94 bldisj 22250 . . . . . . . . . . . 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))) = ∅)
9524, 32, 37, 42, 47, 93, 94syl33anc 1381 . . . . . . . . . . 11 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ (𝑡(ball‘𝐷)(if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2))) = ∅)
96 eqimss 3690 . . . . . . . . . . 11 (((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ (𝑡(ball‘𝐷)(if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2))) = ∅ → ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ (𝑡(ball‘𝐷)(if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2))) ⊆ ∅)
9795, 96syl 17 . . . . . . . . . 10 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ (𝑡(ball‘𝐷)(if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2))) ⊆ ∅)
9897anassrs 681 . . . . . . . . 9 (((𝜑𝑠𝑆) ∧ 𝑡𝑇) → ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ (𝑡(ball‘𝐷)(if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2))) ⊆ ∅)
9998ralrimiva 2995 . . . . . . . 8 ((𝜑𝑠𝑆) → ∀𝑡𝑇 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ (𝑡(ball‘𝐷)(if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2))) ⊆ ∅)
100 iunss 4593 . . . . . . . 8 ( 𝑡𝑇 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ (𝑡(ball‘𝐷)(if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2))) ⊆ ∅ ↔ ∀𝑡𝑇 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ (𝑡(ball‘𝐷)(if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2))) ⊆ ∅)
10199, 100sylibr 224 . . . . . . 7 ((𝜑𝑠𝑆) → 𝑡𝑇 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ (𝑡(ball‘𝐷)(if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2))) ⊆ ∅)
10223, 101syl5eqss 3682 . . . . . 6 ((𝜑𝑠𝑆) → ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ 𝑈) ⊆ ∅)
103102ralrimiva 2995 . . . . 5 (𝜑 → ∀𝑠𝑆 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ 𝑈) ⊆ ∅)
104 iunss 4593 . . . . 5 ( 𝑠𝑆 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ 𝑈) ⊆ ∅ ↔ ∀𝑠𝑆 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ 𝑈) ⊆ ∅)
105103, 104sylibr 224 . . . 4 (𝜑 𝑠𝑆 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ 𝑈) ⊆ ∅)
106 ss0 4007 . . . 4 ( 𝑠𝑆 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ 𝑈) ⊆ ∅ → 𝑠𝑆 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ 𝑈) = ∅)
107105, 106syl 17 . . 3 (𝜑 𝑠𝑆 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ 𝑈) = ∅)
10820, 107syl5eq 2697 . 2 (𝜑 → (𝑉𝑈) = ∅)
109 sseq2 3660 . . . 4 (𝑧 = 𝑉 → (𝑆𝑧𝑆𝑉))
110 ineq1 3840 . . . . 5 (𝑧 = 𝑉 → (𝑧𝑤) = (𝑉𝑤))
111110eqeq1d 2653 . . . 4 (𝑧 = 𝑉 → ((𝑧𝑤) = ∅ ↔ (𝑉𝑤) = ∅))
112109, 1113anbi13d 1441 . . 3 (𝑧 = 𝑉 → ((𝑆𝑧𝑇𝑤 ∧ (𝑧𝑤) = ∅) ↔ (𝑆𝑉𝑇𝑤 ∧ (𝑉𝑤) = ∅)))
113 sseq2 3660 . . . 4 (𝑤 = 𝑈 → (𝑇𝑤𝑇𝑈))
114 ineq2 3841 . . . . 5 (𝑤 = 𝑈 → (𝑉𝑤) = (𝑉𝑈))
115114eqeq1d 2653 . . . 4 (𝑤 = 𝑈 → ((𝑉𝑤) = ∅ ↔ (𝑉𝑈) = ∅))
116113, 1153anbi23d 1442 . . 3 (𝑤 = 𝑈 → ((𝑆𝑉𝑇𝑤 ∧ (𝑉𝑤) = ∅) ↔ (𝑆𝑉𝑇𝑈 ∧ (𝑉𝑈) = ∅)))
117112, 116rspc2ev 3355 . 2 ((𝑉𝐽𝑈𝐽 ∧ (𝑆𝑉𝑇𝑈 ∧ (𝑉𝑈) = ∅)) → ∃𝑧𝐽𝑤𝐽 (𝑆𝑧𝑇𝑤 ∧ (𝑧𝑤) = ∅))
11811, 15, 16, 17, 108, 117syl113anc 1378 1 (𝜑 → ∃𝑧𝐽𝑤𝐽 (𝑆𝑧𝑇𝑤 ∧ (𝑧𝑤) = ∅))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 196  wa 383  w3a 1054   = wceq 1523  wcel 2030  wne 2823  wral 2941  wrex 2942  cin 3606  wss 3607  c0 3948  ifcif 4119   cuni 4468   ciun 4552   class class class wbr 4685  cmpt 4762  ran crn 5144  cfv 5926  (class class class)co 6690  infcinf 8388  cr 9973  0cc0 9974  1c1 9975   + caddc 9977   · cmul 9979  *cxr 10111   < clt 10112  cle 10113   / cdiv 10722  2c2 11108  +crp 11870   +𝑒 cxad 11982   ·e cxmu 11983  ∞Metcxmt 19779  ballcbl 19781  MetOpencmopn 19784  Clsdccld 20868
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-8 2032  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-rep 4804  ax-sep 4814  ax-nul 4822  ax-pow 4873  ax-pr 4936  ax-un 6991  ax-cnex 10030  ax-resscn 10031  ax-1cn 10032  ax-icn 10033  ax-addcl 10034  ax-addrcl 10035  ax-mulcl 10036  ax-mulrcl 10037  ax-mulcom 10038  ax-addass 10039  ax-mulass 10040  ax-distr 10041  ax-i2m1 10042  ax-1ne0 10043  ax-1rid 10044  ax-rnegex 10045  ax-rrecex 10046  ax-cnre 10047  ax-pre-lttri 10048  ax-pre-lttrn 10049  ax-pre-ltadd 10050  ax-pre-mulgt0 10051  ax-pre-sup 10052
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1055  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-ne 2824  df-nel 2927  df-ral 2946  df-rex 2947  df-reu 2948  df-rmo 2949  df-rab 2950  df-v 3233  df-sbc 3469  df-csb 3567  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-pss 3623  df-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-tp 4215  df-op 4217  df-uni 4469  df-int 4508  df-iun 4554  df-iin 4555  df-br 4686  df-opab 4746  df-mpt 4763  df-tr 4786  df-id 5053  df-eprel 5058  df-po 5064  df-so 5065  df-fr 5102  df-we 5104  df-xp 5149  df-rel 5150  df-cnv 5151  df-co 5152  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156  df-pred 5718  df-ord 5764  df-on 5765  df-lim 5766  df-suc 5767  df-iota 5889  df-fun 5928  df-fn 5929  df-f 5930  df-f1 5931  df-fo 5932  df-f1o 5933  df-fv 5934  df-riota 6651  df-ov 6693  df-oprab 6694  df-mpt2 6695  df-om 7108  df-1st 7210  df-2nd 7211  df-wrecs 7452  df-recs 7513  df-rdg 7551  df-er 7787  df-ec 7789  df-map 7901  df-en 7998  df-dom 7999  df-sdom 8000  df-sup 8389  df-inf 8390  df-pnf 10114  df-mnf 10115  df-xr 10116  df-ltxr 10117  df-le 10118  df-sub 10306  df-neg 10307  df-div 10723  df-nn 11059  df-2 11117  df-n0 11331  df-z 11416  df-uz 11726  df-q 11827  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-icc 12220  df-topgen 16151  df-psmet 19786  df-xmet 19787  df-bl 19789  df-mopn 19790  df-top 20747  df-topon 20764  df-bases 20798  df-cld 20871  df-ntr 20872  df-cls 20873
This theorem is referenced by:  metnrm  22712
  Copyright terms: Public domain W3C validator