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

Theorem metdstri 22701
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 811 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → (𝐹𝐴) ∈ ℝ)
2 simprl 809 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → (𝐴𝐷𝐵) ∈ ℝ)
3 rexsub 12102 . . . . . . . . . . . 12 (((𝐹𝐴) ∈ ℝ ∧ (𝐴𝐷𝐵) ∈ ℝ) → ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) = ((𝐹𝐴) − (𝐴𝐷𝐵)))
41, 2, 3syl2anc 694 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) = ((𝐹𝐴) − (𝐴𝐷𝐵)))
54oveq2d 6706 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) = (𝐵(ball‘𝐷)((𝐹𝐴) − (𝐴𝐷𝐵))))
6 simpll 805 . . . . . . . . . . . 12 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → 𝐷 ∈ (∞Met‘𝑋))
76adantr 480 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → 𝐷 ∈ (∞Met‘𝑋))
8 simprr 811 . . . . . . . . . . . 12 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → 𝐵𝑋)
98adantr 480 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → 𝐵𝑋)
10 simprl 809 . . . . . . . . . . . 12 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → 𝐴𝑋)
1110adantr 480 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → 𝐴𝑋)
121, 2resubcld 10496 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → ((𝐹𝐴) − (𝐴𝐷𝐵)) ∈ ℝ)
132leidd 10632 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → (𝐴𝐷𝐵) ≤ (𝐴𝐷𝐵))
14 xmetsym 22199 . . . . . . . . . . . . . . 15 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴𝑋𝐵𝑋) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴))
156, 10, 8, 14syl3anc 1366 . . . . . . . . . . . . . 14 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴))
1615adantr 480 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴))
1716eqcomd 2657 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → (𝐵𝐷𝐴) = (𝐴𝐷𝐵))
181recnd 10106 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → (𝐹𝐴) ∈ ℂ)
192recnd 10106 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → (𝐴𝐷𝐵) ∈ ℂ)
2018, 19nncand 10435 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → ((𝐹𝐴) − ((𝐹𝐴) − (𝐴𝐷𝐵))) = (𝐴𝐷𝐵))
2113, 17, 203brtr4d 4717 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → (𝐵𝐷𝐴) ≤ ((𝐹𝐴) − ((𝐹𝐴) − (𝐴𝐷𝐵))))
22 blss2 22256 . . . . . . . . . . 11 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵𝑋𝐴𝑋) ∧ (((𝐹𝐴) − (𝐴𝐷𝐵)) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ ∧ (𝐵𝐷𝐴) ≤ ((𝐹𝐴) − ((𝐹𝐴) − (𝐴𝐷𝐵))))) → (𝐵(ball‘𝐷)((𝐹𝐴) − (𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹𝐴)))
237, 9, 11, 12, 1, 21, 22syl33anc 1381 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → (𝐵(ball‘𝐷)((𝐹𝐴) − (𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹𝐴)))
245, 23eqsstrd 3672 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹𝐴)))
2524expr 642 . . . . . . . 8 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → ((𝐹𝐴) ∈ ℝ → (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹𝐴))))
266adantr 480 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → 𝐷 ∈ (∞Met‘𝑋))
278adantr 480 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → 𝐵𝑋)
28 metdscn.f . . . . . . . . . . . . . . . . . 18 𝐹 = (𝑥𝑋 ↦ inf(ran (𝑦𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))
2928metdsf 22698 . . . . . . . . . . . . . . . . 17 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) → 𝐹:𝑋⟶(0[,]+∞))
3029adantr 480 . . . . . . . . . . . . . . . 16 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → 𝐹:𝑋⟶(0[,]+∞))
3130, 10ffvelrnd 6400 . . . . . . . . . . . . . . 15 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐹𝐴) ∈ (0[,]+∞))
32 elxrge0 12319 . . . . . . . . . . . . . . . 16 ((𝐹𝐴) ∈ (0[,]+∞) ↔ ((𝐹𝐴) ∈ ℝ* ∧ 0 ≤ (𝐹𝐴)))
3332simplbi 475 . . . . . . . . . . . . . . 15 ((𝐹𝐴) ∈ (0[,]+∞) → (𝐹𝐴) ∈ ℝ*)
3431, 33syl 17 . . . . . . . . . . . . . 14 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐹𝐴) ∈ ℝ*)
3534adantr 480 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → (𝐹𝐴) ∈ ℝ*)
36 xmetcl 22183 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴𝑋𝐵𝑋) → (𝐴𝐷𝐵) ∈ ℝ*)
376, 10, 8, 36syl3anc 1366 . . . . . . . . . . . . . . 15 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐴𝐷𝐵) ∈ ℝ*)
3837adantr 480 . . . . . . . . . . . . . 14 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → (𝐴𝐷𝐵) ∈ ℝ*)
3938xnegcld 12168 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → -𝑒(𝐴𝐷𝐵) ∈ ℝ*)
4035, 39xaddcld 12169 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ∈ ℝ*)
4140adantrr 753 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ∈ ℝ*)
42 pnfxr 10130 . . . . . . . . . . . 12 +∞ ∈ ℝ*
4342a1i 11 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → +∞ ∈ ℝ*)
44 pnfge 12002 . . . . . . . . . . . 12 (((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ∈ ℝ* → ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ +∞)
4541, 44syl 17 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ +∞)
46 ssbl 22275 . . . . . . . . . . 11 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵𝑋) ∧ (((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ +∞) → (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐵(ball‘𝐷)+∞))
4726, 27, 41, 43, 45, 46syl221anc 1377 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐵(ball‘𝐷)+∞))
48 simprr 811 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → (𝐹𝐴) = +∞)
4948oveq2d 6706 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → (𝐴(ball‘𝐷)(𝐹𝐴)) = (𝐴(ball‘𝐷)+∞))
5010adantr 480 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → 𝐴𝑋)
51 simprl 809 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → (𝐴𝐷𝐵) ∈ ℝ)
52 xblpnf 22248 . . . . . . . . . . . . . 14 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴𝑋) → (𝐵 ∈ (𝐴(ball‘𝐷)+∞) ↔ (𝐵𝑋 ∧ (𝐴𝐷𝐵) ∈ ℝ)))
5326, 50, 52syl2anc 694 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → (𝐵 ∈ (𝐴(ball‘𝐷)+∞) ↔ (𝐵𝑋 ∧ (𝐴𝐷𝐵) ∈ ℝ)))
5427, 51, 53mpbir2and 977 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → 𝐵 ∈ (𝐴(ball‘𝐷)+∞))
55 blpnfctr 22288 . . . . . . . . . . . 12 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴𝑋𝐵 ∈ (𝐴(ball‘𝐷)+∞)) → (𝐴(ball‘𝐷)+∞) = (𝐵(ball‘𝐷)+∞))
5626, 50, 54, 55syl3anc 1366 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → (𝐴(ball‘𝐷)+∞) = (𝐵(ball‘𝐷)+∞))
5749, 56eqtr2d 2686 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → (𝐵(ball‘𝐷)+∞) = (𝐴(ball‘𝐷)(𝐹𝐴)))
5847, 57sseqtrd 3674 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹𝐴)))
5958expr 642 . . . . . . . 8 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → ((𝐹𝐴) = +∞ → (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹𝐴))))
6032simprbi 479 . . . . . . . . . . . . 13 ((𝐹𝐴) ∈ (0[,]+∞) → 0 ≤ (𝐹𝐴))
6131, 60syl 17 . . . . . . . . . . . 12 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → 0 ≤ (𝐹𝐴))
62 ge0nemnf 12042 . . . . . . . . . . . 12 (((𝐹𝐴) ∈ ℝ* ∧ 0 ≤ (𝐹𝐴)) → (𝐹𝐴) ≠ -∞)
6334, 61, 62syl2anc 694 . . . . . . . . . . 11 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐹𝐴) ≠ -∞)
6434, 63jca 553 . . . . . . . . . 10 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → ((𝐹𝐴) ∈ ℝ* ∧ (𝐹𝐴) ≠ -∞))
6564adantr 480 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → ((𝐹𝐴) ∈ ℝ* ∧ (𝐹𝐴) ≠ -∞))
66 xrnemnf 11989 . . . . . . . . 9 (((𝐹𝐴) ∈ ℝ* ∧ (𝐹𝐴) ≠ -∞) ↔ ((𝐹𝐴) ∈ ℝ ∨ (𝐹𝐴) = +∞))
6765, 66sylib 208 . . . . . . . 8 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → ((𝐹𝐴) ∈ ℝ ∨ (𝐹𝐴) = +∞))
6825, 59, 67mpjaod 395 . . . . . . 7 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹𝐴)))
69 pnfnlt 12000 . . . . . . . . . . 11 ((𝐹𝐴) ∈ ℝ* → ¬ +∞ < (𝐹𝐴))
7034, 69syl 17 . . . . . . . . . 10 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → ¬ +∞ < (𝐹𝐴))
7170adantr 480 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) = +∞) → ¬ +∞ < (𝐹𝐴))
7237xnegcld 12168 . . . . . . . . . . . . . 14 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → -𝑒(𝐴𝐷𝐵) ∈ ℝ*)
7334, 72xaddcld 12169 . . . . . . . . . . . . 13 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ∈ ℝ*)
74 xbln0 22266 . . . . . . . . . . . . 13 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵𝑋 ∧ ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ∈ ℝ*) → ((𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ≠ ∅ ↔ 0 < ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))))
756, 8, 73, 74syl3anc 1366 . . . . . . . . . . . 12 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → ((𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ≠ ∅ ↔ 0 < ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))))
76 xposdif 12130 . . . . . . . . . . . . 13 (((𝐴𝐷𝐵) ∈ ℝ* ∧ (𝐹𝐴) ∈ ℝ*) → ((𝐴𝐷𝐵) < (𝐹𝐴) ↔ 0 < ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))))
7737, 34, 76syl2anc 694 . . . . . . . . . . . 12 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → ((𝐴𝐷𝐵) < (𝐹𝐴) ↔ 0 < ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))))
7875, 77bitr4d 271 . . . . . . . . . . 11 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → ((𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ≠ ∅ ↔ (𝐴𝐷𝐵) < (𝐹𝐴)))
79 breq1 4688 . . . . . . . . . . 11 ((𝐴𝐷𝐵) = +∞ → ((𝐴𝐷𝐵) < (𝐹𝐴) ↔ +∞ < (𝐹𝐴)))
8078, 79sylan9bb 736 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) = +∞) → ((𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ≠ ∅ ↔ +∞ < (𝐹𝐴)))
8180necon1bbid 2862 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) = +∞) → (¬ +∞ < (𝐹𝐴) ↔ (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) = ∅))
8271, 81mpbid 222 . . . . . . . 8 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) = +∞) → (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) = ∅)
83 0ss 4005 . . . . . . . 8 ∅ ⊆ (𝐴(ball‘𝐷)(𝐹𝐴))
8482, 83syl6eqss 3688 . . . . . . 7 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) = +∞) → (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹𝐴)))
85 xmetge0 22196 . . . . . . . . . . 11 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴𝑋𝐵𝑋) → 0 ≤ (𝐴𝐷𝐵))
866, 10, 8, 85syl3anc 1366 . . . . . . . . . 10 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → 0 ≤ (𝐴𝐷𝐵))
87 ge0nemnf 12042 . . . . . . . . . 10 (((𝐴𝐷𝐵) ∈ ℝ* ∧ 0 ≤ (𝐴𝐷𝐵)) → (𝐴𝐷𝐵) ≠ -∞)
8837, 86, 87syl2anc 694 . . . . . . . . 9 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐴𝐷𝐵) ≠ -∞)
8937, 88jca 553 . . . . . . . 8 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → ((𝐴𝐷𝐵) ∈ ℝ* ∧ (𝐴𝐷𝐵) ≠ -∞))
90 xrnemnf 11989 . . . . . . . 8 (((𝐴𝐷𝐵) ∈ ℝ* ∧ (𝐴𝐷𝐵) ≠ -∞) ↔ ((𝐴𝐷𝐵) ∈ ℝ ∨ (𝐴𝐷𝐵) = +∞))
9189, 90sylib 208 . . . . . . 7 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → ((𝐴𝐷𝐵) ∈ ℝ ∨ (𝐴𝐷𝐵) = +∞))
9268, 84, 91mpjaodan 844 . . . . . 6 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹𝐴)))
93 sslin 3872 . . . . . 6 ((𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹𝐴)) → (𝑆 ∩ (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)))) ⊆ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹𝐴))))
9492, 93syl 17 . . . . 5 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝑆 ∩ (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)))) ⊆ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹𝐴))))
95 xrleid 12021 . . . . . . 7 ((𝐹𝐴) ∈ ℝ* → (𝐹𝐴) ≤ (𝐹𝐴))
9634, 95syl 17 . . . . . 6 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐹𝐴) ≤ (𝐹𝐴))
97 simplr 807 . . . . . . 7 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → 𝑆𝑋)
9828metdsge 22699 . . . . . . 7 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) ∈ ℝ*) → ((𝐹𝐴) ≤ (𝐹𝐴) ↔ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹𝐴))) = ∅))
996, 97, 10, 34, 98syl31anc 1369 . . . . . 6 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → ((𝐹𝐴) ≤ (𝐹𝐴) ↔ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹𝐴))) = ∅))
10096, 99mpbid 222 . . . . 5 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹𝐴))) = ∅)
101 sseq0 4008 . . . . 5 (((𝑆 ∩ (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)))) ⊆ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹𝐴))) ∧ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹𝐴))) = ∅) → (𝑆 ∩ (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)))) = ∅)
10294, 100, 101syl2anc 694 . . . 4 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝑆 ∩ (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)))) = ∅)
10328metdsge 22699 . . . . 5 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐵𝑋) ∧ ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ∈ ℝ*) → (((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ (𝐹𝐵) ↔ (𝑆 ∩ (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)))) = ∅))
1046, 97, 8, 73, 103syl31anc 1369 . . . 4 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ (𝐹𝐵) ↔ (𝑆 ∩ (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)))) = ∅))
105102, 104mpbird 247 . . 3 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ (𝐹𝐵))
10630, 8ffvelrnd 6400 . . . . 5 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐹𝐵) ∈ (0[,]+∞))
107 elxrge0 12319 . . . . . 6 ((𝐹𝐵) ∈ (0[,]+∞) ↔ ((𝐹𝐵) ∈ ℝ* ∧ 0 ≤ (𝐹𝐵)))
108107simplbi 475 . . . . 5 ((𝐹𝐵) ∈ (0[,]+∞) → (𝐹𝐵) ∈ ℝ*)
109106, 108syl 17 . . . 4 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐹𝐵) ∈ ℝ*)
110107simprbi 479 . . . . 5 ((𝐹𝐵) ∈ (0[,]+∞) → 0 ≤ (𝐹𝐵))
111106, 110syl 17 . . . 4 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → 0 ≤ (𝐹𝐵))
112 xlesubadd 12131 . . . 4 ((((𝐹𝐴) ∈ ℝ* ∧ (𝐴𝐷𝐵) ∈ ℝ* ∧ (𝐹𝐵) ∈ ℝ*) ∧ (0 ≤ (𝐹𝐴) ∧ (𝐴𝐷𝐵) ≠ -∞ ∧ 0 ≤ (𝐹𝐵))) → (((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ (𝐹𝐵) ↔ (𝐹𝐴) ≤ ((𝐹𝐵) +𝑒 (𝐴𝐷𝐵))))
11334, 37, 109, 61, 88, 111, 112syl33anc 1381 . . 3 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ (𝐹𝐵) ↔ (𝐹𝐴) ≤ ((𝐹𝐵) +𝑒 (𝐴𝐷𝐵))))
114105, 113mpbid 222 . 2 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐹𝐴) ≤ ((𝐹𝐵) +𝑒 (𝐴𝐷𝐵)))
115 xaddcom 12109 . . 3 (((𝐹𝐵) ∈ ℝ* ∧ (𝐴𝐷𝐵) ∈ ℝ*) → ((𝐹𝐵) +𝑒 (𝐴𝐷𝐵)) = ((𝐴𝐷𝐵) +𝑒 (𝐹𝐵)))
116109, 37, 115syl2anc 694 . 2 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → ((𝐹𝐵) +𝑒 (𝐴𝐷𝐵)) = ((𝐴𝐷𝐵) +𝑒 (𝐹𝐵)))
117114, 116breqtrd 4711 1 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐹𝐴) ≤ ((𝐴𝐷𝐵) +𝑒 (𝐹𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 382  wa 383   = wceq 1523  wcel 2030  wne 2823  cin 3606  wss 3607  c0 3948   class class class wbr 4685  cmpt 4762  ran crn 5144  wf 5922  cfv 5926  (class class class)co 6690  infcinf 8388  cr 9973  0cc0 9974  +∞cpnf 10109  -∞cmnf 10110  *cxr 10111   < clt 10112  cle 10113  cmin 10304  -𝑒cxne 11981   +𝑒 cxad 11982  [,]cicc 12216  ∞Metcxmt 19779  ballcbl 19781
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-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-nul 3949  df-if 4120  df-pw 4193  df-sn 4211  df-pr 4213  df-op 4217  df-uni 4469  df-iun 4554  df-br 4686  df-opab 4746  df-mpt 4763  df-id 5053  df-po 5064  df-so 5065  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-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-1st 7210  df-2nd 7211  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-2 11117  df-rp 11871  df-xneg 11984  df-xadd 11985  df-xmul 11986  df-icc 12220  df-psmet 19786  df-xmet 19787  df-bl 19789
This theorem is referenced by:  metdsle  22702  metdscnlem  22705  metnrmlem1  22709
  Copyright terms: Public domain W3C validator