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

Theorem metdstri 22557
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 795 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → (𝐹𝐴) ∈ ℝ)
2 simprl 793 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → (𝐴𝐷𝐵) ∈ ℝ)
3 rexsub 12006 . . . . . . . . . . . 12 (((𝐹𝐴) ∈ ℝ ∧ (𝐴𝐷𝐵) ∈ ℝ) → ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) = ((𝐹𝐴) − (𝐴𝐷𝐵)))
41, 2, 3syl2anc 692 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) = ((𝐹𝐴) − (𝐴𝐷𝐵)))
54oveq2d 6621 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) = (𝐵(ball‘𝐷)((𝐹𝐴) − (𝐴𝐷𝐵))))
6 simpll 789 . . . . . . . . . . . 12 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → 𝐷 ∈ (∞Met‘𝑋))
76adantr 481 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → 𝐷 ∈ (∞Met‘𝑋))
8 simprr 795 . . . . . . . . . . . 12 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → 𝐵𝑋)
98adantr 481 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → 𝐵𝑋)
10 simprl 793 . . . . . . . . . . . 12 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → 𝐴𝑋)
1110adantr 481 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → 𝐴𝑋)
121, 2resubcld 10403 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → ((𝐹𝐴) − (𝐴𝐷𝐵)) ∈ ℝ)
132leidd 10539 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → (𝐴𝐷𝐵) ≤ (𝐴𝐷𝐵))
14 xmetsym 22057 . . . . . . . . . . . . . . 15 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴𝑋𝐵𝑋) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴))
156, 10, 8, 14syl3anc 1323 . . . . . . . . . . . . . 14 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴))
1615adantr 481 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴))
1716eqcomd 2632 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → (𝐵𝐷𝐴) = (𝐴𝐷𝐵))
181recnd 10013 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → (𝐹𝐴) ∈ ℂ)
192recnd 10013 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → (𝐴𝐷𝐵) ∈ ℂ)
2018, 19nncand 10342 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → ((𝐹𝐴) − ((𝐹𝐴) − (𝐴𝐷𝐵))) = (𝐴𝐷𝐵))
2113, 17, 203brtr4d 4650 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → (𝐵𝐷𝐴) ≤ ((𝐹𝐴) − ((𝐹𝐴) − (𝐴𝐷𝐵))))
22 blss2 22114 . . . . . . . . . . 11 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵𝑋𝐴𝑋) ∧ (((𝐹𝐴) − (𝐴𝐷𝐵)) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ ∧ (𝐵𝐷𝐴) ≤ ((𝐹𝐴) − ((𝐹𝐴) − (𝐴𝐷𝐵))))) → (𝐵(ball‘𝐷)((𝐹𝐴) − (𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹𝐴)))
237, 9, 11, 12, 1, 21, 22syl33anc 1338 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → (𝐵(ball‘𝐷)((𝐹𝐴) − (𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹𝐴)))
245, 23eqsstrd 3623 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) ∈ ℝ)) → (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹𝐴)))
2524expr 642 . . . . . . . 8 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → ((𝐹𝐴) ∈ ℝ → (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹𝐴))))
266adantr 481 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → 𝐷 ∈ (∞Met‘𝑋))
278adantr 481 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → 𝐵𝑋)
28 metdscn.f . . . . . . . . . . . . . . . . . 18 𝐹 = (𝑥𝑋 ↦ inf(ran (𝑦𝑆 ↦ (𝑥𝐷𝑦)), ℝ*, < ))
2928metdsf 22554 . . . . . . . . . . . . . . . . 17 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) → 𝐹:𝑋⟶(0[,]+∞))
3029adantr 481 . . . . . . . . . . . . . . . 16 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → 𝐹:𝑋⟶(0[,]+∞))
3130, 10ffvelrnd 6317 . . . . . . . . . . . . . . 15 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐹𝐴) ∈ (0[,]+∞))
32 elxrge0 12220 . . . . . . . . . . . . . . . 16 ((𝐹𝐴) ∈ (0[,]+∞) ↔ ((𝐹𝐴) ∈ ℝ* ∧ 0 ≤ (𝐹𝐴)))
3332simplbi 476 . . . . . . . . . . . . . . 15 ((𝐹𝐴) ∈ (0[,]+∞) → (𝐹𝐴) ∈ ℝ*)
3431, 33syl 17 . . . . . . . . . . . . . 14 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐹𝐴) ∈ ℝ*)
3534adantr 481 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → (𝐹𝐴) ∈ ℝ*)
36 xmetcl 22041 . . . . . . . . . . . . . . . 16 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴𝑋𝐵𝑋) → (𝐴𝐷𝐵) ∈ ℝ*)
376, 10, 8, 36syl3anc 1323 . . . . . . . . . . . . . . 15 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐴𝐷𝐵) ∈ ℝ*)
3837adantr 481 . . . . . . . . . . . . . 14 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → (𝐴𝐷𝐵) ∈ ℝ*)
3938xnegcld 12070 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → -𝑒(𝐴𝐷𝐵) ∈ ℝ*)
4035, 39xaddcld 12071 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ∈ ℝ*)
4140adantrr 752 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ∈ ℝ*)
42 pnfxr 10037 . . . . . . . . . . . 12 +∞ ∈ ℝ*
4342a1i 11 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → +∞ ∈ ℝ*)
44 pnfge 11908 . . . . . . . . . . . 12 (((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ∈ ℝ* → ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ +∞)
4541, 44syl 17 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ +∞)
46 ssbl 22133 . . . . . . . . . . 11 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵𝑋) ∧ (((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ∈ ℝ* ∧ +∞ ∈ ℝ*) ∧ ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ +∞) → (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐵(ball‘𝐷)+∞))
4726, 27, 41, 43, 45, 46syl221anc 1334 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐵(ball‘𝐷)+∞))
48 simprr 795 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → (𝐹𝐴) = +∞)
4948oveq2d 6621 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → (𝐴(ball‘𝐷)(𝐹𝐴)) = (𝐴(ball‘𝐷)+∞))
5010adantr 481 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → 𝐴𝑋)
51 simprl 793 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → (𝐴𝐷𝐵) ∈ ℝ)
52 xblpnf 22106 . . . . . . . . . . . . . 14 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴𝑋) → (𝐵 ∈ (𝐴(ball‘𝐷)+∞) ↔ (𝐵𝑋 ∧ (𝐴𝐷𝐵) ∈ ℝ)))
5326, 50, 52syl2anc 692 . . . . . . . . . . . . 13 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → (𝐵 ∈ (𝐴(ball‘𝐷)+∞) ↔ (𝐵𝑋 ∧ (𝐴𝐷𝐵) ∈ ℝ)))
5427, 51, 53mpbir2and 956 . . . . . . . . . . . 12 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → 𝐵 ∈ (𝐴(ball‘𝐷)+∞))
55 blpnfctr 22146 . . . . . . . . . . . 12 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴𝑋𝐵 ∈ (𝐴(ball‘𝐷)+∞)) → (𝐴(ball‘𝐷)+∞) = (𝐵(ball‘𝐷)+∞))
5626, 50, 54, 55syl3anc 1323 . . . . . . . . . . 11 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → (𝐴(ball‘𝐷)+∞) = (𝐵(ball‘𝐷)+∞))
5749, 56eqtr2d 2661 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → (𝐵(ball‘𝐷)+∞) = (𝐴(ball‘𝐷)(𝐹𝐴)))
5847, 57sseqtrd 3625 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ ((𝐴𝐷𝐵) ∈ ℝ ∧ (𝐹𝐴) = +∞)) → (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹𝐴)))
5958expr 642 . . . . . . . 8 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → ((𝐹𝐴) = +∞ → (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹𝐴))))
6032simprbi 480 . . . . . . . . . . . . 13 ((𝐹𝐴) ∈ (0[,]+∞) → 0 ≤ (𝐹𝐴))
6131, 60syl 17 . . . . . . . . . . . 12 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → 0 ≤ (𝐹𝐴))
62 ge0nemnf 11946 . . . . . . . . . . . 12 (((𝐹𝐴) ∈ ℝ* ∧ 0 ≤ (𝐹𝐴)) → (𝐹𝐴) ≠ -∞)
6334, 61, 62syl2anc 692 . . . . . . . . . . 11 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐹𝐴) ≠ -∞)
6434, 63jca 554 . . . . . . . . . 10 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → ((𝐹𝐴) ∈ ℝ* ∧ (𝐹𝐴) ≠ -∞))
6564adantr 481 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → ((𝐹𝐴) ∈ ℝ* ∧ (𝐹𝐴) ≠ -∞))
66 xrnemnf 11895 . . . . . . . . 9 (((𝐹𝐴) ∈ ℝ* ∧ (𝐹𝐴) ≠ -∞) ↔ ((𝐹𝐴) ∈ ℝ ∨ (𝐹𝐴) = +∞))
6765, 66sylib 208 . . . . . . . 8 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → ((𝐹𝐴) ∈ ℝ ∨ (𝐹𝐴) = +∞))
6825, 59, 67mpjaod 396 . . . . . . 7 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) ∈ ℝ) → (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹𝐴)))
69 pnfnlt 11906 . . . . . . . . . . 11 ((𝐹𝐴) ∈ ℝ* → ¬ +∞ < (𝐹𝐴))
7034, 69syl 17 . . . . . . . . . 10 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → ¬ +∞ < (𝐹𝐴))
7170adantr 481 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) = +∞) → ¬ +∞ < (𝐹𝐴))
7237xnegcld 12070 . . . . . . . . . . . . . 14 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → -𝑒(𝐴𝐷𝐵) ∈ ℝ*)
7334, 72xaddcld 12071 . . . . . . . . . . . . 13 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ∈ ℝ*)
74 xbln0 22124 . . . . . . . . . . . . 13 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵𝑋 ∧ ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ∈ ℝ*) → ((𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ≠ ∅ ↔ 0 < ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))))
756, 8, 73, 74syl3anc 1323 . . . . . . . . . . . 12 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → ((𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ≠ ∅ ↔ 0 < ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))))
76 xposdif 12032 . . . . . . . . . . . . 13 (((𝐴𝐷𝐵) ∈ ℝ* ∧ (𝐹𝐴) ∈ ℝ*) → ((𝐴𝐷𝐵) < (𝐹𝐴) ↔ 0 < ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))))
7737, 34, 76syl2anc 692 . . . . . . . . . . . 12 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → ((𝐴𝐷𝐵) < (𝐹𝐴) ↔ 0 < ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))))
7875, 77bitr4d 271 . . . . . . . . . . 11 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → ((𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ≠ ∅ ↔ (𝐴𝐷𝐵) < (𝐹𝐴)))
79 breq1 4621 . . . . . . . . . . 11 ((𝐴𝐷𝐵) = +∞ → ((𝐴𝐷𝐵) < (𝐹𝐴) ↔ +∞ < (𝐹𝐴)))
8078, 79sylan9bb 735 . . . . . . . . . 10 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) = +∞) → ((𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ≠ ∅ ↔ +∞ < (𝐹𝐴)))
8180necon1bbid 2835 . . . . . . . . 9 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) = +∞) → (¬ +∞ < (𝐹𝐴) ↔ (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) = ∅))
8271, 81mpbid 222 . . . . . . . 8 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) = +∞) → (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) = ∅)
83 0ss 3949 . . . . . . . 8 ∅ ⊆ (𝐴(ball‘𝐷)(𝐹𝐴))
8482, 83syl6eqss 3639 . . . . . . 7 ((((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) ∧ (𝐴𝐷𝐵) = +∞) → (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹𝐴)))
85 xmetge0 22054 . . . . . . . . . . 11 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴𝑋𝐵𝑋) → 0 ≤ (𝐴𝐷𝐵))
866, 10, 8, 85syl3anc 1323 . . . . . . . . . 10 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → 0 ≤ (𝐴𝐷𝐵))
87 ge0nemnf 11946 . . . . . . . . . 10 (((𝐴𝐷𝐵) ∈ ℝ* ∧ 0 ≤ (𝐴𝐷𝐵)) → (𝐴𝐷𝐵) ≠ -∞)
8837, 86, 87syl2anc 692 . . . . . . . . 9 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐴𝐷𝐵) ≠ -∞)
8937, 88jca 554 . . . . . . . 8 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → ((𝐴𝐷𝐵) ∈ ℝ* ∧ (𝐴𝐷𝐵) ≠ -∞))
90 xrnemnf 11895 . . . . . . . 8 (((𝐴𝐷𝐵) ∈ ℝ* ∧ (𝐴𝐷𝐵) ≠ -∞) ↔ ((𝐴𝐷𝐵) ∈ ℝ ∨ (𝐴𝐷𝐵) = +∞))
9189, 90sylib 208 . . . . . . 7 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → ((𝐴𝐷𝐵) ∈ ℝ ∨ (𝐴𝐷𝐵) = +∞))
9268, 84, 91mpjaodan 826 . . . . . 6 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹𝐴)))
93 sslin 3822 . . . . . 6 ((𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵))) ⊆ (𝐴(ball‘𝐷)(𝐹𝐴)) → (𝑆 ∩ (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)))) ⊆ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹𝐴))))
9492, 93syl 17 . . . . 5 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝑆 ∩ (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)))) ⊆ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹𝐴))))
95 xrleid 11927 . . . . . . 7 ((𝐹𝐴) ∈ ℝ* → (𝐹𝐴) ≤ (𝐹𝐴))
9634, 95syl 17 . . . . . 6 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐹𝐴) ≤ (𝐹𝐴))
97 simplr 791 . . . . . . 7 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → 𝑆𝑋)
9828metdsge 22555 . . . . . . 7 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐴𝑋) ∧ (𝐹𝐴) ∈ ℝ*) → ((𝐹𝐴) ≤ (𝐹𝐴) ↔ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹𝐴))) = ∅))
996, 97, 10, 34, 98syl31anc 1326 . . . . . 6 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → ((𝐹𝐴) ≤ (𝐹𝐴) ↔ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹𝐴))) = ∅))
10096, 99mpbid 222 . . . . 5 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹𝐴))) = ∅)
101 sseq0 3952 . . . . 5 (((𝑆 ∩ (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)))) ⊆ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹𝐴))) ∧ (𝑆 ∩ (𝐴(ball‘𝐷)(𝐹𝐴))) = ∅) → (𝑆 ∩ (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)))) = ∅)
10294, 100, 101syl2anc 692 . . . 4 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝑆 ∩ (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)))) = ∅)
10328metdsge 22555 . . . . 5 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋𝐵𝑋) ∧ ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ∈ ℝ*) → (((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ (𝐹𝐵) ↔ (𝑆 ∩ (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)))) = ∅))
1046, 97, 8, 73, 103syl31anc 1326 . . . 4 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ (𝐹𝐵) ↔ (𝑆 ∩ (𝐵(ball‘𝐷)((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)))) = ∅))
105102, 104mpbird 247 . . 3 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → ((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ (𝐹𝐵))
10630, 8ffvelrnd 6317 . . . . 5 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐹𝐵) ∈ (0[,]+∞))
107 elxrge0 12220 . . . . . 6 ((𝐹𝐵) ∈ (0[,]+∞) ↔ ((𝐹𝐵) ∈ ℝ* ∧ 0 ≤ (𝐹𝐵)))
108107simplbi 476 . . . . 5 ((𝐹𝐵) ∈ (0[,]+∞) → (𝐹𝐵) ∈ ℝ*)
109106, 108syl 17 . . . 4 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐹𝐵) ∈ ℝ*)
110107simprbi 480 . . . . 5 ((𝐹𝐵) ∈ (0[,]+∞) → 0 ≤ (𝐹𝐵))
111106, 110syl 17 . . . 4 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → 0 ≤ (𝐹𝐵))
112 xlesubadd 12033 . . . 4 ((((𝐹𝐴) ∈ ℝ* ∧ (𝐴𝐷𝐵) ∈ ℝ* ∧ (𝐹𝐵) ∈ ℝ*) ∧ (0 ≤ (𝐹𝐴) ∧ (𝐴𝐷𝐵) ≠ -∞ ∧ 0 ≤ (𝐹𝐵))) → (((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ (𝐹𝐵) ↔ (𝐹𝐴) ≤ ((𝐹𝐵) +𝑒 (𝐴𝐷𝐵))))
11334, 37, 109, 61, 88, 111, 112syl33anc 1338 . . 3 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (((𝐹𝐴) +𝑒 -𝑒(𝐴𝐷𝐵)) ≤ (𝐹𝐵) ↔ (𝐹𝐴) ≤ ((𝐹𝐵) +𝑒 (𝐴𝐷𝐵))))
114105, 113mpbid 222 . 2 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐹𝐴) ≤ ((𝐹𝐵) +𝑒 (𝐴𝐷𝐵)))
115 xaddcom 12013 . . 3 (((𝐹𝐵) ∈ ℝ* ∧ (𝐴𝐷𝐵) ∈ ℝ*) → ((𝐹𝐵) +𝑒 (𝐴𝐷𝐵)) = ((𝐴𝐷𝐵) +𝑒 (𝐹𝐵)))
116109, 37, 115syl2anc 692 . 2 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → ((𝐹𝐵) +𝑒 (𝐴𝐷𝐵)) = ((𝐴𝐷𝐵) +𝑒 (𝐹𝐵)))
117114, 116breqtrd 4644 1 (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆𝑋) ∧ (𝐴𝑋𝐵𝑋)) → (𝐹𝐴) ≤ ((𝐴𝐷𝐵) +𝑒 (𝐹𝐵)))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 196  wo 383  wa 384   = wceq 1480  wcel 1992  wne 2796  cin 3559  wss 3560  c0 3896   class class class wbr 4618  cmpt 4678  ran crn 5080  wf 5846  cfv 5850  (class class class)co 6605  infcinf 8292  cr 9880  0cc0 9881  +∞cpnf 10016  -∞cmnf 10017  *cxr 10018   < clt 10019  cle 10020  cmin 10211  -𝑒cxne 11887   +𝑒 cxad 11888  [,]cicc 12117  ∞Metcxmt 19645  ballcbl 19647
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1841  ax-6 1890  ax-7 1937  ax-8 1994  ax-9 2001  ax-10 2021  ax-11 2036  ax-12 2049  ax-13 2250  ax-ext 2606  ax-sep 4746  ax-nul 4754  ax-pow 4808  ax-pr 4872  ax-un 6903  ax-cnex 9937  ax-resscn 9938  ax-1cn 9939  ax-icn 9940  ax-addcl 9941  ax-addrcl 9942  ax-mulcl 9943  ax-mulrcl 9944  ax-mulcom 9945  ax-addass 9946  ax-mulass 9947  ax-distr 9948  ax-i2m1 9949  ax-1ne0 9950  ax-1rid 9951  ax-rnegex 9952  ax-rrecex 9953  ax-cnre 9954  ax-pre-lttri 9955  ax-pre-lttrn 9956  ax-pre-ltadd 9957  ax-pre-mulgt0 9958  ax-pre-sup 9959
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3or 1037  df-3an 1038  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1883  df-eu 2478  df-mo 2479  df-clab 2613  df-cleq 2619  df-clel 2622  df-nfc 2756  df-ne 2797  df-nel 2900  df-ral 2917  df-rex 2918  df-reu 2919  df-rmo 2920  df-rab 2921  df-v 3193  df-sbc 3423  df-csb 3520  df-dif 3563  df-un 3565  df-in 3567  df-ss 3574  df-nul 3897  df-if 4064  df-pw 4137  df-sn 4154  df-pr 4156  df-op 4160  df-uni 4408  df-iun 4492  df-br 4619  df-opab 4679  df-mpt 4680  df-id 4994  df-po 5000  df-so 5001  df-xp 5085  df-rel 5086  df-cnv 5087  df-co 5088  df-dm 5089  df-rn 5090  df-res 5091  df-ima 5092  df-iota 5813  df-fun 5852  df-fn 5853  df-f 5854  df-f1 5855  df-fo 5856  df-f1o 5857  df-fv 5858  df-riota 6566  df-ov 6608  df-oprab 6609  df-mpt2 6610  df-1st 7116  df-2nd 7117  df-er 7688  df-ec 7690  df-map 7805  df-en 7901  df-dom 7902  df-sdom 7903  df-sup 8293  df-inf 8294  df-pnf 10021  df-mnf 10022  df-xr 10023  df-ltxr 10024  df-le 10025  df-sub 10213  df-neg 10214  df-div 10630  df-2 11024  df-rp 11777  df-xneg 11890  df-xadd 11891  df-xmul 11892  df-icc 12121  df-psmet 19652  df-xmet 19653  df-bl 19655
This theorem is referenced by:  metdsle  22558  metdscnlem  22561  metnrmlem1  22565
  Copyright terms: Public domain W3C validator