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

Theorem metnrmlem3 22786
 Description: Lemma for metnrm 22787. (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 3913 . . . . 5 (𝑇𝑆) = (𝑆𝑇)
7 metnrmlem.4 . . . . 5 (𝜑 → (𝑆𝑇) = ∅)
86, 7syl5eq 2770 . . . 4 (𝜑 → (𝑇𝑆) = ∅)
9 metnrmlem.v . . . 4 𝑉 = 𝑠𝑆 (𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2))
101, 2, 3, 4, 5, 8, 9metnrmlem2 22785 . . 3 (𝜑 → (𝑉𝐽𝑆𝑉))
1110simpld 477 . 2 (𝜑𝑉𝐽)
12 metdscn.f . . . 4 𝐹 = (𝑥𝑋 ↦ inf(ran (𝑦𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))
13 metnrmlem.u . . . 4 𝑈 = 𝑡𝑇 (𝑡(ball‘𝐷)(if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2))
1412, 2, 3, 5, 4, 7, 13metnrmlem2 22785 . . 3 (𝜑 → (𝑈𝐽𝑇𝑈))
1514simpld 477 . 2 (𝜑𝑈𝐽)
1610simprd 482 . 2 (𝜑𝑆𝑉)
1714simprd 482 . 2 (𝜑𝑇𝑈)
189ineq1i 3918 . . . 4 (𝑉𝑈) = ( 𝑠𝑆 (𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ 𝑈)
19 iunin1 4693 . . . 4 𝑠𝑆 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ 𝑈) = ( 𝑠𝑆 (𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ 𝑈)
2018, 19eqtr4i 2749 . . 3 (𝑉𝑈) = 𝑠𝑆 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ 𝑈)
2113ineq2i 3919 . . . . . . . 8 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ 𝑈) = ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ 𝑡𝑇 (𝑡(ball‘𝐷)(if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2)))
22 iunin2 4692 . . . . . . . 8 𝑡𝑇 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ (𝑡(ball‘𝐷)(if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2))) = ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ 𝑡𝑇 (𝑡(ball‘𝐷)(if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2)))
2321, 22eqtr4i 2749 . . . . . . 7 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ 𝑈) = 𝑡𝑇 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ (𝑡(ball‘𝐷)(if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2)))
243adantr 472 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → 𝐷 ∈ (∞Met‘𝑋))
25 eqid 2724 . . . . . . . . . . . . . . . . 17 𝐽 = 𝐽
2625cldss 20956 . . . . . . . . . . . . . . . 16 (𝑆 ∈ (Clsd‘𝐽) → 𝑆 𝐽)
275, 26syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑆 𝐽)
282mopnuni 22368 . . . . . . . . . . . . . . . 16 (𝐷 ∈ (∞Met‘𝑋) → 𝑋 = 𝐽)
293, 28syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑋 = 𝐽)
3027, 29sseqtr4d 3748 . . . . . . . . . . . . . 14 (𝜑𝑆𝑋)
3130sselda 3709 . . . . . . . . . . . . 13 ((𝜑𝑠𝑆) → 𝑠𝑋)
3231adantrr 755 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → 𝑠𝑋)
3325cldss 20956 . . . . . . . . . . . . . . . 16 (𝑇 ∈ (Clsd‘𝐽) → 𝑇 𝐽)
344, 33syl 17 . . . . . . . . . . . . . . 15 (𝜑𝑇 𝐽)
3534, 29sseqtr4d 3748 . . . . . . . . . . . . . 14 (𝜑𝑇𝑋)
3635sselda 3709 . . . . . . . . . . . . 13 ((𝜑𝑡𝑇) → 𝑡𝑋)
3736adantrl 754 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → 𝑡𝑋)
381, 2, 3, 4, 5, 8metnrmlem1a 22783 . . . . . . . . . . . . . . . 16 ((𝜑𝑠𝑆) → (0 < (𝐺𝑠) ∧ if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) ∈ ℝ+))
3938simprd 482 . . . . . . . . . . . . . . 15 ((𝜑𝑠𝑆) → if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) ∈ ℝ+)
4039adantrr 755 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) ∈ ℝ+)
4140rphalfcld 11998 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2) ∈ ℝ+)
4241rpxrd 11987 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2) ∈ ℝ*)
4312, 2, 3, 5, 4, 7metnrmlem1a 22783 . . . . . . . . . . . . . . . 16 ((𝜑𝑡𝑇) → (0 < (𝐹𝑡) ∧ if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) ∈ ℝ+))
4443adantrl 754 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (0 < (𝐹𝑡) ∧ if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) ∈ ℝ+))
4544simprd 482 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) ∈ ℝ+)
4645rphalfcld 11998 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2) ∈ ℝ+)
4746rpxrd 11987 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2) ∈ ℝ*)
4840rpred 11986 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) ∈ ℝ)
4948rehalfcld 11392 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2) ∈ ℝ)
5045rpred 11986 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) ∈ ℝ)
5150rehalfcld 11392 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2) ∈ ℝ)
52 rexadd 12177 . . . . . . . . . . . . . . 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 696 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2) +𝑒 (if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2)) = ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2) + (if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2)))
5448recnd 10181 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) ∈ ℂ)
5550recnd 10181 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) ∈ ℂ)
56 2cnd 11206 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → 2 ∈ ℂ)
57 2ne0 11226 . . . . . . . . . . . . . . . 16 2 ≠ 0
5857a1i 11 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → 2 ≠ 0)
5954, 55, 56, 58divdird 10952 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) + if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))) / 2) = ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2) + (if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2)))
6053, 59eqtr4d 2761 . . . . . . . . . . . . 13 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2) +𝑒 (if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2)) = ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) + if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))) / 2))
611, 2, 3, 4, 5, 8metnrmlem1 22784 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑡𝑇𝑠𝑆)) → if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) ≤ (𝑡𝐷𝑠))
6261ancom2s 879 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) ≤ (𝑡𝐷𝑠))
63 xmetsym 22274 . . . . . . . . . . . . . . . . . 18 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑡𝑋𝑠𝑋) → (𝑡𝐷𝑠) = (𝑠𝐷𝑡))
6424, 37, 32, 63syl3anc 1439 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (𝑡𝐷𝑠) = (𝑠𝐷𝑡))
6562, 64breqtrd 4786 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) ≤ (𝑠𝐷𝑡))
6612, 2, 3, 5, 4, 7metnrmlem1 22784 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) ≤ (𝑠𝐷𝑡))
6740rpxrd 11987 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) ∈ ℝ*)
6845rpxrd 11987 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) ∈ ℝ*)
69 xmetcl 22258 . . . . . . . . . . . . . . . . . 18 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑠𝑋𝑡𝑋) → (𝑠𝐷𝑡) ∈ ℝ*)
7024, 32, 37, 69syl3anc 1439 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (𝑠𝐷𝑡) ∈ ℝ*)
71 xle2add 12203 . . . . . . . . . . . . . . . . 17 (((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) ∈ ℝ* ∧ if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) ∈ ℝ*) ∧ ((𝑠𝐷𝑡) ∈ ℝ* ∧ (𝑠𝐷𝑡) ∈ ℝ*)) → ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) ≤ (𝑠𝐷𝑡) ∧ if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) ≤ (𝑠𝐷𝑡)) → (if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) +𝑒 if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))) ≤ ((𝑠𝐷𝑡) +𝑒 (𝑠𝐷𝑡))))
7267, 68, 70, 70, 71syl22anc 1440 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) ≤ (𝑠𝐷𝑡) ∧ if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) ≤ (𝑠𝐷𝑡)) → (if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) +𝑒 if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))) ≤ ((𝑠𝐷𝑡) +𝑒 (𝑠𝐷𝑡))))
7365, 66, 72mp2and 717 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) +𝑒 if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))) ≤ ((𝑠𝐷𝑡) +𝑒 (𝑠𝐷𝑡)))
7448, 50readdcld 10182 . . . . . . . . . . . . . . . . . 18 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) + if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))) ∈ ℝ)
7574recnd 10181 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) + if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))) ∈ ℂ)
7675, 56, 58divcan2d 10916 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (2 · ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) + if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))) / 2)) = (if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) + if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))))
77 2re 11203 . . . . . . . . . . . . . . . . 17 2 ∈ ℝ
7874rehalfcld 11392 . . . . . . . . . . . . . . . . 17 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) + if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))) / 2) ∈ ℝ)
79 rexmul 12215 . . . . . . . . . . . . . . . . 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 698 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (2 ·e ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) + if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))) / 2)) = (2 · ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) + if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))) / 2)))
81 rexadd 12177 . . . . . . . . . . . . . . . . 17 ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) ∈ ℝ ∧ if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) ∈ ℝ) → (if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) +𝑒 if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))) = (if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) + if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))))
8248, 50, 81syl2anc 696 . . . . . . . . . . . . . . . 16 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) +𝑒 if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))) = (if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) + if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))))
8376, 80, 823eqtr4d 2768 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (2 ·e ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) + if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))) / 2)) = (if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) +𝑒 if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))))
84 x2times 12243 . . . . . . . . . . . . . . . 16 ((𝑠𝐷𝑡) ∈ ℝ* → (2 ·e (𝑠𝐷𝑡)) = ((𝑠𝐷𝑡) +𝑒 (𝑠𝐷𝑡)))
8570, 84syl 17 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (2 ·e (𝑠𝐷𝑡)) = ((𝑠𝐷𝑡) +𝑒 (𝑠𝐷𝑡)))
8673, 83, 853brtr4d 4792 . . . . . . . . . . . . . 14 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → (2 ·e ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) + if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))) / 2)) ≤ (2 ·e (𝑠𝐷𝑡)))
8778rexrd 10202 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) + if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡))) / 2) ∈ ℝ*)
88 2rp 11951 . . . . . . . . . . . . . . . 16 2 ∈ ℝ+
8988a1i 11 . . . . . . . . . . . . . . 15 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → 2 ∈ ℝ+)
90 xlemul2 12235 . . . . . . . . . . . . . . 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 1439 . . . . . . . . . . . . . 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 4782 . . . . . . . . . . . 12 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → ((if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2) +𝑒 (if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2)) ≤ (𝑠𝐷𝑡))
94 bldisj 22325 . . . . . . . . . . . 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 1454 . . . . . . . . . . 11 ((𝜑 ∧ (𝑠𝑆𝑡𝑇)) → ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ (𝑡(ball‘𝐷)(if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2))) = ∅)
96 eqimss 3763 . . . . . . . . . . 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 683 . . . . . . . . 9 (((𝜑𝑠𝑆) ∧ 𝑡𝑇) → ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ (𝑡(ball‘𝐷)(if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2))) ⊆ ∅)
9998ralrimiva 3068 . . . . . . . 8 ((𝜑𝑠𝑆) → ∀𝑡𝑇 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ (𝑡(ball‘𝐷)(if(1 ≤ (𝐹𝑡), 1, (𝐹𝑡)) / 2))) ⊆ ∅)
100 iunss 4669 . . . . . . . 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 3755 . . . . . 6 ((𝜑𝑠𝑆) → ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ 𝑈) ⊆ ∅)
103102ralrimiva 3068 . . . . 5 (𝜑 → ∀𝑠𝑆 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ 𝑈) ⊆ ∅)
104 iunss 4669 . . . . 5 ( 𝑠𝑆 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ 𝑈) ⊆ ∅ ↔ ∀𝑠𝑆 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ 𝑈) ⊆ ∅)
105103, 104sylibr 224 . . . 4 (𝜑 𝑠𝑆 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ 𝑈) ⊆ ∅)
106 ss0 4082 . . . 4 ( 𝑠𝑆 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ 𝑈) ⊆ ∅ → 𝑠𝑆 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ 𝑈) = ∅)
107105, 106syl 17 . . 3 (𝜑 𝑠𝑆 ((𝑠(ball‘𝐷)(if(1 ≤ (𝐺𝑠), 1, (𝐺𝑠)) / 2)) ∩ 𝑈) = ∅)
10820, 107syl5eq 2770 . 2 (𝜑 → (𝑉𝑈) = ∅)
109 sseq2 3733 . . . 4 (𝑧 = 𝑉 → (𝑆𝑧𝑆𝑉))
110 ineq1 3915 . . . . 5 (𝑧 = 𝑉 → (𝑧𝑤) = (𝑉𝑤))
111110eqeq1d 2726 . . . 4 (𝑧 = 𝑉 → ((𝑧𝑤) = ∅ ↔ (𝑉𝑤) = ∅))
112109, 1113anbi13d 1514 . . 3 (𝑧 = 𝑉 → ((𝑆𝑧𝑇𝑤 ∧ (𝑧𝑤) = ∅) ↔ (𝑆𝑉𝑇𝑤 ∧ (𝑉𝑤) = ∅)))
113 sseq2 3733 . . . 4 (𝑤 = 𝑈 → (𝑇𝑤𝑇𝑈))
114 ineq2 3916 . . . . 5 (𝑤 = 𝑈 → (𝑉𝑤) = (𝑉𝑈))
115114eqeq1d 2726 . . . 4 (𝑤 = 𝑈 → ((𝑉𝑤) = ∅ ↔ (𝑉𝑈) = ∅))
116113, 1153anbi23d 1515 . . 3 (𝑤 = 𝑈 → ((𝑆𝑉𝑇𝑤 ∧ (𝑉𝑤) = ∅) ↔ (𝑆𝑉𝑇𝑈 ∧ (𝑉𝑈) = ∅)))
117112, 116rspc2ev 3428 . 2 ((𝑉𝐽𝑈𝐽 ∧ (𝑆𝑉𝑇𝑈 ∧ (𝑉𝑈) = ∅)) → ∃𝑧𝐽𝑤𝐽 (𝑆𝑧𝑇𝑤 ∧ (𝑧𝑤) = ∅))
11811, 15, 16, 17, 108, 117syl113anc 1451 1 (𝜑 → ∃𝑧𝐽𝑤𝐽 (𝑆𝑧𝑇𝑤 ∧ (𝑧𝑤) = ∅))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 196   ∧ wa 383   ∧ w3a 1072   = wceq 1596   ∈ wcel 2103   ≠ wne 2896  ∀wral 3014  ∃wrex 3015   ∩ cin 3679   ⊆ wss 3680  ∅c0 4023  ifcif 4194  ∪ cuni 4544  ∪ ciun 4628   class class class wbr 4760   ↦ cmpt 4837  ran crn 5219  ‘cfv 6001  (class class class)co 6765  infcinf 8463  ℝcr 10048  0cc0 10049  1c1 10050   + caddc 10052   · cmul 10054  ℝ*cxr 10186   < clt 10187   ≤ cle 10188   / cdiv 10797  2c2 11183  ℝ+crp 11946   +𝑒 cxad 12058   ·e cxmu 12059  ∞Metcxmt 19854  ballcbl 19856  MetOpencmopn 19859  Clsdccld 20943 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-8 2105  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704  ax-rep 4879  ax-sep 4889  ax-nul 4897  ax-pow 4948  ax-pr 5011  ax-un 7066  ax-cnex 10105  ax-resscn 10106  ax-1cn 10107  ax-icn 10108  ax-addcl 10109  ax-addrcl 10110  ax-mulcl 10111  ax-mulrcl 10112  ax-mulcom 10113  ax-addass 10114  ax-mulass 10115  ax-distr 10116  ax-i2m1 10117  ax-1ne0 10118  ax-1rid 10119  ax-rnegex 10120  ax-rrecex 10121  ax-cnre 10122  ax-pre-lttri 10123  ax-pre-lttrn 10124  ax-pre-ltadd 10125  ax-pre-mulgt0 10126  ax-pre-sup 10127 This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3or 1073  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-eu 2575  df-mo 2576  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-ne 2897  df-nel 3000  df-ral 3019  df-rex 3020  df-reu 3021  df-rmo 3022  df-rab 3023  df-v 3306  df-sbc 3542  df-csb 3640  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-pss 3696  df-nul 4024  df-if 4195  df-pw 4268  df-sn 4286  df-pr 4288  df-tp 4290  df-op 4292  df-uni 4545  df-int 4584  df-iun 4630  df-iin 4631  df-br 4761  df-opab 4821  df-mpt 4838  df-tr 4861  df-id 5128  df-eprel 5133  df-po 5139  df-so 5140  df-fr 5177  df-we 5179  df-xp 5224  df-rel 5225  df-cnv 5226  df-co 5227  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231  df-pred 5793  df-ord 5839  df-on 5840  df-lim 5841  df-suc 5842  df-iota 5964  df-fun 6003  df-fn 6004  df-f 6005  df-f1 6006  df-fo 6007  df-f1o 6008  df-fv 6009  df-riota 6726  df-ov 6768  df-oprab 6769  df-mpt2 6770  df-om 7183  df-1st 7285  df-2nd 7286  df-wrecs 7527  df-recs 7588  df-rdg 7626  df-er 7862  df-ec 7864  df-map 7976  df-en 8073  df-dom 8074  df-sdom 8075  df-sup 8464  df-inf 8465  df-pnf 10189  df-mnf 10190  df-xr 10191  df-ltxr 10192  df-le 10193  df-sub 10381  df-neg 10382  df-div 10798  df-nn 11134  df-2 11192  df-n0 11406  df-z 11491  df-uz 11801  df-q 11903  df-rp 11947  df-xneg 12060  df-xadd 12061  df-xmul 12062  df-icc 12296  df-topgen 16227  df-psmet 19861  df-xmet 19862  df-bl 19864  df-mopn 19865  df-top 20822  df-topon 20839  df-bases 20873  df-cld 20946  df-ntr 20947  df-cls 20948 This theorem is referenced by:  metnrm  22787
 Copyright terms: Public domain W3C validator