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

Theorem metdstri 24873
Description: A generalization of the triangle inequality to the point-set distance function. Under the usual notation where the same symbol 𝑑 denotes the point-point and point-set distance functions, this theorem would be written 𝑑(𝑎, 𝑆) ≤ 𝑑(𝑎, 𝑏) + 𝑑(𝑏, 𝑆). (Contributed by Mario Carneiro, 4-Sep-2015.)
Hypothesis
Ref Expression
metdscn.f 𝐹 = (𝑥𝑋 ↦ inf(ran (𝑦𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))
Assertion
Ref Expression
metdstri (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐹𝐴) ≤ ((𝐴𝐷𝐵) +𝑒 (𝐹𝐵)))
Distinct variable groups:   𝑥,𝑦,𝐴   𝑥,𝐷,𝑦   𝑥,𝐵,𝑦   𝑥,𝑆,𝑦   𝑥,𝑋,𝑦
Allowed substitution hints:   𝐹(𝑥,𝑦)

Proof of Theorem metdstri
StepHypRef Expression
1 simprr 773 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → (𝐹𝐴) ∈ ℝ)
2 simprl 771 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → (𝐴𝐷𝐵) ∈ ℝ)
3 rexsub 13275 . . . . . . . . . . . 12 (((𝐹𝐴) ∈ ℝ ∧ (𝐴𝐷𝐵) ∈ ℝ) → ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) = ((𝐹𝐴) − (𝐴𝐷𝐵)))
41, 2, 3syl2anc 584 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) = ((𝐹𝐴) − (𝐴𝐷𝐵)))
54oveq2d 7447 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) = (𝐵(ball‘𝐷)((𝐹𝐴) − (𝐴𝐷𝐵))))
6 simpll 767 . . . . . . . . . . . 12 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → 𝐷 ∈ (∞Met‘𝑋))
76adantr 480 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → 𝐷 ∈ (∞Met‘𝑋))
8 simprr 773 . . . . . . . . . . . 12 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → 𝐵𝑋)
98adantr 480 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → 𝐵𝑋)
10 simprl 771 . . . . . . . . . . . 12 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → 𝐴𝑋)
1110adantr 480 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → 𝐴𝑋)
121, 2resubcld 11691 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → ((𝐹𝐴) − (𝐴𝐷𝐵)) ∈ ℝ)
132leidd 11829 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → (𝐴𝐷𝐵) ≤ (𝐴𝐷𝐵))
14 xmetsym 24357 . . . . . . . . . . . . . . 15 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴𝑋𝐵𝑋) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴))
156, 10, 8, 14syl3anc 1373 . . . . . . . . . . . . . 14 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴))
1615adantr 480 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴))
1716eqcomd 2743 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → (𝐵𝐷𝐴) = (𝐴𝐷𝐵))
181recnd 11289 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → (𝐹𝐴) ∈ ℂ)
192recnd 11289 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → (𝐴𝐷𝐵) ∈ ℂ)
2018, 19nncand 11625 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → ((𝐹𝐴) − ((𝐹𝐴) − (𝐴𝐷𝐵))) = (𝐴𝐷𝐵))
2113, 17, 203brtr4d 5175 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → (𝐵𝐷𝐴) ≤ ((𝐹𝐴) − ((𝐹𝐴) − (𝐴𝐷𝐵))))
22 blss2 24414 . . . . . . . . . . 11 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵𝑋𝐴𝑋) ∧ (((𝐹𝐴) − (𝐴𝐷𝐵)) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ ∧ (𝐵𝐷𝐴) ≤ ((𝐹𝐴) − ((𝐹𝐴) − (𝐴𝐷𝐵))))) → (𝐵(ball‘𝐷)((𝐹𝐴) − (𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹𝐴)))
237, 9, 11, 12, 1, 21, 22syl33anc 1387 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → (𝐵(ball‘𝐷)((𝐹𝐴) − (𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹𝐴)))
245, 23eqsstrd 4018 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹𝐴)))
2524expr 456 . . . . . . . 8 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → ((𝐹𝐴) ∈ ℝ → (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹𝐴))))
266adantr 480 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → 𝐷 ∈ (∞Met‘𝑋))
278adantr 480 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → 𝐵𝑋)
28 metdscn.f . . . . . . . . . . . . . . . . . 18 𝐹 = (𝑥𝑋 ↦ inf(ran (𝑦𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))
2928metdsf 24870 . . . . . . . . . . . . . . . . 17 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) → 𝐹:𝑋⟶(0[,]+∞))
3029adantr 480 . . . . . . . . . . . . . . . 16 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → 𝐹:𝑋⟶(0[,]+∞))
3130, 10ffvelcdmd 7105 . . . . . . . . . . . . . . 15 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐹𝐴) ∈ (0[,]+∞))
32 eliccxr 13475 . . . . . . . . . . . . . . 15 ((𝐹𝐴) ∈ (0[,]+∞) → (𝐹𝐴) ∈ ℝ*)
3331, 32syl 17 . . . . . . . . . . . . . 14 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐹𝐴) ∈ ℝ*)
3433adantr 480 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → (𝐹𝐴) ∈ ℝ*)
35 xmetcl 24341 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴𝑋𝐵𝑋) → (𝐴𝐷𝐵) ∈ ℝ*)
366, 10, 8, 35syl3anc 1373 . . . . . . . . . . . . . . 15 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐴𝐷𝐵) ∈ ℝ*)
3736adantr 480 . . . . . . . . . . . . . 14 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → (𝐴𝐷𝐵) ∈ ℝ*)
3837xnegcld 13342 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → -𝑒(𝐴𝐷𝐵) ∈ ℝ*)
3934, 38xaddcld 13343 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ∈ ℝ*)
4039adantrr 717 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ∈ ℝ*)
41 pnfxr 11315 . . . . . . . . . . . 12 +∞ ∈ ℝ*
4241a1i 11 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → +∞ ∈ ℝ*)
43 pnfge 13172 . . . . . . . . . . . 12 (((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ∈ ℝ* → ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ +∞)
4440, 43syl 17 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ +∞)
45 ssbl 24433 . . . . . . . . . . 11 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵𝑋) ∧ (((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ +∞) → (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐵(ball‘𝐷)+∞))
4626, 27, 40, 42, 44, 45syl221anc 1383 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐵(ball‘𝐷)+∞))
47 simprr 773 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → (𝐹𝐴) = +∞)
4847oveq2d 7447 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → (𝐴(ball‘𝐷)(𝐹𝐴)) = (𝐴(ball‘𝐷)+∞))
4910adantr 480 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → 𝐴𝑋)
50 simprl 771 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → (𝐴𝐷𝐵) ∈ ℝ)
51 xblpnf 24406 . . . . . . . . . . . . . 14 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴𝑋) → (𝐵 ∈ (𝐴(ball‘𝐷)+∞) ↔ (𝐵𝑋 ∧ (𝐴𝐷𝐵) ∈ ℝ)))
5226, 49, 51syl2anc 584 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → (𝐵 ∈ (𝐴(ball‘𝐷)+∞) ↔ (𝐵𝑋 ∧ (𝐴𝐷𝐵) ∈ ℝ)))
5327, 50, 52mpbir2and 713 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → 𝐵 ∈ (𝐴(ball‘𝐷)+∞))
54 blpnfctr 24446 . . . . . . . . . . . 12 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴𝑋𝐵 ∈ (𝐴(ball‘𝐷)+∞)) → (𝐴(ball‘𝐷)+∞) = (𝐵(ball‘𝐷)+∞))
5526, 49, 53, 54syl3anc 1373 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → (𝐴(ball‘𝐷)+∞) = (𝐵(ball‘𝐷)+∞))
5648, 55eqtr2d 2778 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → (𝐵(ball‘𝐷)+∞) = (𝐴(ball‘𝐷)(𝐹𝐴)))
5746, 56sseqtrd 4020 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹𝐴)))
5857expr 456 . . . . . . . 8 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → ((𝐹𝐴) = +∞ → (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹𝐴))))
59 elxrge0 13497 . . . . . . . . . . . . . 14 ((𝐹𝐴) ∈ (0[,]+∞) ↔ ((𝐹𝐴) ∈ ℝ* ∧ 0 ≤ (𝐹𝐴)))
6059simprbi 496 . . . . . . . . . . . . 13 ((𝐹𝐴) ∈ (0[,]+∞) → 0 ≤ (𝐹𝐴))
6131, 60syl 17 . . . . . . . . . . . 12 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → 0 ≤ (𝐹𝐴))
62 ge0nemnf 13215 . . . . . . . . . . . 12 (((𝐹𝐴) ∈ ℝ* ∧ 0 ≤ (𝐹𝐴)) → (𝐹𝐴) ≠ -∞)
6333, 61, 62syl2anc 584 . . . . . . . . . . 11 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐹𝐴) ≠ -∞)
6433, 63jca 511 . . . . . . . . . 10 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → ((𝐹𝐴) ∈ ℝ* ∧ (𝐹𝐴) ≠ -∞))
6564adantr 480 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → ((𝐹𝐴) ∈ ℝ* ∧ (𝐹𝐴) ≠ -∞))
66 xrnemnf 13159 . . . . . . . . 9 (((𝐹𝐴) ∈ ℝ* ∧ (𝐹𝐴) ≠ -∞) ↔ ((𝐹𝐴) ∈ ℝ ∨ (𝐹𝐴) = +∞))
6765, 66sylib 218 . . . . . . . 8 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → ((𝐹𝐴) ∈ ℝ ∨ (𝐹𝐴) = +∞))
6825, 58, 67mpjaod 861 . . . . . . 7 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹𝐴)))
69 pnfnlt 13170 . . . . . . . . . . 11 ((𝐹𝐴) ∈ ℝ* → ¬ +∞ < (𝐹𝐴))
7033, 69syl 17 . . . . . . . . . 10 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → ¬ +∞ < (𝐹𝐴))
7170adantr 480 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) = +∞) → ¬ +∞ < (𝐹𝐴))
7236xnegcld 13342 . . . . . . . . . . . . . 14 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → -𝑒(𝐴𝐷𝐵) ∈ ℝ*)
7333, 72xaddcld 13343 . . . . . . . . . . . . 13 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ∈ ℝ*)
74 xbln0 24424 . . . . . . . . . . . . 13 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵𝑋 ∧ ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ∈ ℝ*) → ((𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ≠ ∅ ↔ 0 < ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))))
756, 8, 73, 74syl3anc 1373 . . . . . . . . . . . 12 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → ((𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ≠ ∅ ↔ 0 < ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))))
76 xposdif 13304 . . . . . . . . . . . . 13 (((𝐴𝐷𝐵) ∈ ℝ* ∧ (𝐹𝐴) ∈ ℝ*) → ((𝐴𝐷𝐵) < (𝐹𝐴) ↔ 0 < ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))))
7736, 33, 76syl2anc 584 . . . . . . . . . . . 12 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → ((𝐴𝐷𝐵) < (𝐹𝐴) ↔ 0 < ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))))
7875, 77bitr4d 282 . . . . . . . . . . 11 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → ((𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ≠ ∅ ↔ (𝐴𝐷𝐵) < (𝐹𝐴)))
79 breq1 5146 . . . . . . . . . . 11 ((𝐴𝐷𝐵) = +∞ → ((𝐴𝐷𝐵) < (𝐹𝐴) ↔ +∞ < (𝐹𝐴)))
8078, 79sylan9bb 509 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) = +∞) → ((𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ≠ ∅ ↔ +∞ < (𝐹𝐴)))
8180necon1bbid 2980 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) = +∞) → (¬ +∞ < (𝐹𝐴) ↔ (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) = ∅))
8271, 81mpbid 232 . . . . . . . 8 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) = +∞) → (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) = ∅)
83 0ss 4400 . . . . . . . 8 ∅ ⊆ (𝐴(ball‘𝐷)(𝐹𝐴))
8482, 83eqsstrdi 4028 . . . . . . 7 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) = +∞) → (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹𝐴)))
85 xmetge0 24354 . . . . . . . . . . 11 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴𝑋𝐵𝑋) → 0 ≤ (𝐴𝐷𝐵))
866, 10, 8, 85syl3anc 1373 . . . . . . . . . 10 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → 0 ≤ (𝐴𝐷𝐵))
87 ge0nemnf 13215 . . . . . . . . . 10 (((𝐴𝐷𝐵) ∈ ℝ* ∧ 0 ≤ (𝐴𝐷𝐵)) → (𝐴𝐷𝐵) ≠ -∞)
8836, 86, 87syl2anc 584 . . . . . . . . 9 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐴𝐷𝐵) ≠ -∞)
8936, 88jca 511 . . . . . . . 8 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → ((𝐴𝐷𝐵) ∈ ℝ* ∧ (𝐴𝐷𝐵) ≠ -∞))
90 xrnemnf 13159 . . . . . . . 8 (((𝐴𝐷𝐵) ∈ ℝ* ∧ (𝐴𝐷𝐵) ≠ -∞) ↔ ((𝐴𝐷𝐵) ∈ ℝ ∨ (𝐴𝐷𝐵) = +∞))
9189, 90sylib 218 . . . . . . 7 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → ((𝐴𝐷𝐵) ∈ ℝ ∨ (𝐴𝐷𝐵) = +∞))
9268, 84, 91mpjaodan 961 . . . . . 6 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹𝐴)))
93 sslin 4243 . . . . . 6 ((𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹𝐴)) → (𝑆 ∩ (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)))) ⊆ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹𝐴))))
9492, 93syl 17 . . . . 5 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝑆 ∩ (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)))) ⊆ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹𝐴))))
9533xrleidd 13194 . . . . . 6 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐹𝐴) ≤ (𝐹𝐴))
96 simplr 769 . . . . . . 7 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → 𝑆𝑋)
9728metdsge 24871 . . . . . . 7 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) ∈ ℝ*) → ((𝐹𝐴) ≤ (𝐹𝐴) ↔ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹𝐴))) = ∅))
986, 96, 10, 33, 97syl31anc 1375 . . . . . 6 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → ((𝐹𝐴) ≤ (𝐹𝐴) ↔ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹𝐴))) = ∅))
9995, 98mpbid 232 . . . . 5 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹𝐴))) = ∅)
100 sseq0 4403 . . . . 5 (((𝑆 ∩ (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)))) ⊆ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹𝐴))) ∧ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹𝐴))) = ∅) → (𝑆 ∩ (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)))) = ∅)
10194, 99, 100syl2anc 584 . . . 4 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝑆 ∩ (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)))) = ∅)
10228metdsge 24871 . . . . 5 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐵𝑋) ∧ ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ∈ ℝ*) → (((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ (𝐹𝐵) ↔ (𝑆 ∩ (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)))) = ∅))
1036, 96, 8, 73, 102syl31anc 1375 . . . 4 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ (𝐹𝐵) ↔ (𝑆 ∩ (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)))) = ∅))
104101, 103mpbird 257 . . 3 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ (𝐹𝐵))
10530, 8ffvelcdmd 7105 . . . . 5 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐹𝐵) ∈ (0[,]+∞))
106 eliccxr 13475 . . . . 5 ((𝐹𝐵) ∈ (0[,]+∞) → (𝐹𝐵) ∈ ℝ*)
107105, 106syl 17 . . . 4 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐹𝐵) ∈ ℝ*)
108 elxrge0 13497 . . . . . 6 ((𝐹𝐵) ∈ (0[,]+∞) ↔ ((𝐹𝐵) ∈ ℝ* ∧ 0 ≤ (𝐹𝐵)))
109108simprbi 496 . . . . 5 ((𝐹𝐵) ∈ (0[,]+∞) → 0 ≤ (𝐹𝐵))
110105, 109syl 17 . . . 4 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → 0 ≤ (𝐹𝐵))
111 xlesubadd 13305 . . . 4 ((((𝐹𝐴) ∈ ℝ* ∧ (𝐴𝐷𝐵) ∈ ℝ* ∧ (𝐹𝐵) ∈ ℝ*) ∧ (0 ≤ (𝐹𝐴) ∧ (𝐴𝐷𝐵) ≠ -∞ ∧ 0 ≤ (𝐹𝐵))) → (((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ (𝐹𝐵) ↔ (𝐹𝐴) ≤ ((𝐹𝐵) +𝑒 (𝐴𝐷𝐵))))
11233, 36, 107, 61, 88, 110, 111syl33anc 1387 . . 3 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ (𝐹𝐵) ↔ (𝐹𝐴) ≤ ((𝐹𝐵) +𝑒 (𝐴𝐷𝐵))))
113104, 112mpbid 232 . 2 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐹𝐴) ≤ ((𝐹𝐵) +𝑒 (𝐴𝐷𝐵)))
114 xaddcom 13282 . . 3 (((𝐹𝐵) ∈ ℝ* ∧ (𝐴𝐷𝐵) ∈ ℝ*) → ((𝐹𝐵) +𝑒 (𝐴𝐷𝐵)) = ((𝐴𝐷𝐵) +𝑒 (𝐹𝐵)))
115107, 36, 114syl2anc 584 . 2 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → ((𝐹𝐵) +𝑒 (𝐴𝐷𝐵)) = ((𝐴𝐷𝐵) +𝑒 (𝐹𝐵)))
116113, 115breqtrd 5169 1 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐹𝐴) ≤ ((𝐴𝐷𝐵) +𝑒 (𝐹𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wa 395  wo 848   = wceq 1540  wcel 2108  wne 2940  cin 3950  wss 3951  c0 4333   class class class wbr 5143  cmpt 5225  ran crn 5686  wf 6557  cfv 6561  (class class class)co 7431  infcinf 9481  cr 11154  0cc0 11155  +∞cpnf 11292  -∞cmnf 11293  *cxr 11294   < clt 11295  cle 11296  cmin 11492  -𝑒cxne 13151   +𝑒 cxad 13152  [,]cicc 13390  ∞Metcxmet 21349  ballcbl 21351
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pow 5365  ax-pr 5432  ax-un 7755  ax-cnex 11211  ax-resscn 11212  ax-1cn 11213  ax-icn 11214  ax-addcl 11215  ax-addrcl 11216  ax-mulcl 11217  ax-mulrcl 11218  ax-mulcom 11219  ax-addass 11220  ax-mulass 11221  ax-distr 11222  ax-i2m1 11223  ax-1ne0 11224  ax-1rid 11225  ax-rnegex 11226  ax-rrecex 11227  ax-cnre 11228  ax-pre-lttri 11229  ax-pre-lttrn 11230  ax-pre-ltadd 11231  ax-pre-mulgt0 11232  ax-pre-sup 11233
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3or 1088  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2540  df-eu 2569  df-clab 2715  df-cleq 2729  df-clel 2816  df-nfc 2892  df-ne 2941  df-nel 3047  df-ral 3062  df-rex 3071  df-rmo 3380  df-reu 3381  df-rab 3437  df-v 3482  df-sbc 3789  df-csb 3900  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-pw 4602  df-sn 4627  df-pr 4629  df-op 4633  df-uni 4908  df-iun 4993  df-br 5144  df-opab 5206  df-mpt 5226  df-id 5578  df-po 5592  df-so 5593  df-xp 5691  df-rel 5692  df-cnv 5693  df-co 5694  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698  df-iota 6514  df-fun 6563  df-fn 6564  df-f 6565  df-f1 6566  df-fo 6567  df-f1o 6568  df-fv 6569  df-riota 7388  df-ov 7434  df-oprab 7435  df-mpo 7436  df-1st 8014  df-2nd 8015  df-er 8745  df-ec 8747  df-map 8868  df-en 8986  df-dom 8987  df-sdom 8988  df-sup 9482  df-inf 9483  df-pnf 11297  df-mnf 11298  df-xr 11299  df-ltxr 11300  df-le 11301  df-sub 11494  df-neg 11495  df-div 11921  df-2 12329  df-rp 13035  df-xneg 13154  df-xadd 13155  df-xmul 13156  df-icc 13394  df-psmet 21356  df-xmet 21357  df-bl 21359
This theorem is referenced by:  metdsle  24874  metdscnlem  24877  metnrmlem1  24881
  Copyright terms: Public domain W3C validator