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

Theorem blval2 23278
 Description: The ball around a point 𝑃, alternative definition. (Contributed by Thierry Arnoux, 7-Dec-2017.) (Revised by Thierry Arnoux, 11-Mar-2018.)
Assertion
Ref Expression
blval2 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃𝑋𝑅 ∈ ℝ+) → (𝑃(ball‘𝐷)𝑅) = ((𝐷 “ (0[,)𝑅)) “ {𝑃}))

Proof of Theorem blval2
Dummy variable 𝑥 is distinct from all other variables.
StepHypRef Expression
1 rpxr 12452 . . 3 (𝑅 ∈ ℝ+𝑅 ∈ ℝ*)
2 blvalps 23101 . . 3 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃𝑋𝑅 ∈ ℝ*) → (𝑃(ball‘𝐷)𝑅) = {𝑥𝑋 ∣ (𝑃𝐷𝑥) < 𝑅})
31, 2syl3an3 1162 . 2 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃𝑋𝑅 ∈ ℝ+) → (𝑃(ball‘𝐷)𝑅) = {𝑥𝑋 ∣ (𝑃𝐷𝑥) < 𝑅})
4 nfv 1915 . . 3 𝑥(𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃𝑋𝑅 ∈ ℝ+)
5 nfcv 2919 . . 3 𝑥((𝐷 “ (0[,)𝑅)) “ {𝑃})
6 nfrab1 3302 . . 3 𝑥{𝑥𝑋 ∣ (𝑃𝐷𝑥) < 𝑅}
7 psmetf 23022 . . . . . . 7 (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
8 ffn 6503 . . . . . . 7 (𝐷:(𝑋 × 𝑋)⟶ℝ*𝐷 Fn (𝑋 × 𝑋))
9 elpreima 6824 . . . . . . 7 (𝐷 Fn (𝑋 × 𝑋) → (⟨𝑃, 𝑥⟩ ∈ (𝐷 “ (0[,)𝑅)) ↔ (⟨𝑃, 𝑥⟩ ∈ (𝑋 × 𝑋) ∧ (𝐷‘⟨𝑃, 𝑥⟩) ∈ (0[,)𝑅))))
107, 8, 93syl 18 . . . . . 6 (𝐷 ∈ (PsMet‘𝑋) → (⟨𝑃, 𝑥⟩ ∈ (𝐷 “ (0[,)𝑅)) ↔ (⟨𝑃, 𝑥⟩ ∈ (𝑋 × 𝑋) ∧ (𝐷‘⟨𝑃, 𝑥⟩) ∈ (0[,)𝑅))))
11103ad2ant1 1130 . . . . 5 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃𝑋𝑅 ∈ ℝ+) → (⟨𝑃, 𝑥⟩ ∈ (𝐷 “ (0[,)𝑅)) ↔ (⟨𝑃, 𝑥⟩ ∈ (𝑋 × 𝑋) ∧ (𝐷‘⟨𝑃, 𝑥⟩) ∈ (0[,)𝑅))))
12 opelxp 5564 . . . . . . . . . 10 (⟨𝑃, 𝑥⟩ ∈ (𝑋 × 𝑋) ↔ (𝑃𝑋𝑥𝑋))
1312baib 539 . . . . . . . . 9 (𝑃𝑋 → (⟨𝑃, 𝑥⟩ ∈ (𝑋 × 𝑋) ↔ 𝑥𝑋))
14133ad2ant2 1131 . . . . . . . 8 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃𝑋𝑅 ∈ ℝ+) → (⟨𝑃, 𝑥⟩ ∈ (𝑋 × 𝑋) ↔ 𝑥𝑋))
1514biimpd 232 . . . . . . 7 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃𝑋𝑅 ∈ ℝ+) → (⟨𝑃, 𝑥⟩ ∈ (𝑋 × 𝑋) → 𝑥𝑋))
1615adantrd 495 . . . . . 6 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃𝑋𝑅 ∈ ℝ+) → ((⟨𝑃, 𝑥⟩ ∈ (𝑋 × 𝑋) ∧ (𝐷‘⟨𝑃, 𝑥⟩) ∈ (0[,)𝑅)) → 𝑥𝑋))
17 simprl 770 . . . . . . 7 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃𝑋𝑅 ∈ ℝ+) ∧ (𝑥𝑋 ∧ (𝑃𝐷𝑥) < 𝑅)) → 𝑥𝑋)
1817ex 416 . . . . . 6 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃𝑋𝑅 ∈ ℝ+) → ((𝑥𝑋 ∧ (𝑃𝐷𝑥) < 𝑅) → 𝑥𝑋))
19 simpl2 1189 . . . . . . . . 9 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃𝑋𝑅 ∈ ℝ+) ∧ 𝑥𝑋) → 𝑃𝑋)
2019, 13syl 17 . . . . . . . 8 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃𝑋𝑅 ∈ ℝ+) ∧ 𝑥𝑋) → (⟨𝑃, 𝑥⟩ ∈ (𝑋 × 𝑋) ↔ 𝑥𝑋))
21 df-ov 7159 . . . . . . . . . 10 (𝑃𝐷𝑥) = (𝐷‘⟨𝑃, 𝑥⟩)
2221eleq1i 2842 . . . . . . . . 9 ((𝑃𝐷𝑥) ∈ (0[,)𝑅) ↔ (𝐷‘⟨𝑃, 𝑥⟩) ∈ (0[,)𝑅))
23 0xr 10739 . . . . . . . . . . 11 0 ∈ ℝ*
24 simpl3 1190 . . . . . . . . . . . 12 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃𝑋𝑅 ∈ ℝ+) ∧ 𝑥𝑋) → 𝑅 ∈ ℝ+)
2524rpxrd 12486 . . . . . . . . . . 11 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃𝑋𝑅 ∈ ℝ+) ∧ 𝑥𝑋) → 𝑅 ∈ ℝ*)
26 elico1 12835 . . . . . . . . . . 11 ((0 ∈ ℝ*𝑅 ∈ ℝ*) → ((𝑃𝐷𝑥) ∈ (0[,)𝑅) ↔ ((𝑃𝐷𝑥) ∈ ℝ* ∧ 0 ≤ (𝑃𝐷𝑥) ∧ (𝑃𝐷𝑥) < 𝑅)))
2723, 25, 26sylancr 590 . . . . . . . . . 10 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃𝑋𝑅 ∈ ℝ+) ∧ 𝑥𝑋) → ((𝑃𝐷𝑥) ∈ (0[,)𝑅) ↔ ((𝑃𝐷𝑥) ∈ ℝ* ∧ 0 ≤ (𝑃𝐷𝑥) ∧ (𝑃𝐷𝑥) < 𝑅)))
28 df-3an 1086 . . . . . . . . . . 11 (((𝑃𝐷𝑥) ∈ ℝ* ∧ 0 ≤ (𝑃𝐷𝑥) ∧ (𝑃𝐷𝑥) < 𝑅) ↔ (((𝑃𝐷𝑥) ∈ ℝ* ∧ 0 ≤ (𝑃𝐷𝑥)) ∧ (𝑃𝐷𝑥) < 𝑅))
29 simpl1 1188 . . . . . . . . . . . . . 14 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃𝑋𝑅 ∈ ℝ+) ∧ 𝑥𝑋) → 𝐷 ∈ (PsMet‘𝑋))
30 simpr 488 . . . . . . . . . . . . . 14 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃𝑋𝑅 ∈ ℝ+) ∧ 𝑥𝑋) → 𝑥𝑋)
31 psmetcl 23023 . . . . . . . . . . . . . 14 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃𝑋𝑥𝑋) → (𝑃𝐷𝑥) ∈ ℝ*)
3229, 19, 30, 31syl3anc 1368 . . . . . . . . . . . . 13 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃𝑋𝑅 ∈ ℝ+) ∧ 𝑥𝑋) → (𝑃𝐷𝑥) ∈ ℝ*)
33 psmetge0 23028 . . . . . . . . . . . . . 14 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃𝑋𝑥𝑋) → 0 ≤ (𝑃𝐷𝑥))
3429, 19, 30, 33syl3anc 1368 . . . . . . . . . . . . 13 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃𝑋𝑅 ∈ ℝ+) ∧ 𝑥𝑋) → 0 ≤ (𝑃𝐷𝑥))
3532, 34jca 515 . . . . . . . . . . . 12 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃𝑋𝑅 ∈ ℝ+) ∧ 𝑥𝑋) → ((𝑃𝐷𝑥) ∈ ℝ* ∧ 0 ≤ (𝑃𝐷𝑥)))
3635biantrurd 536 . . . . . . . . . . 11 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃𝑋𝑅 ∈ ℝ+) ∧ 𝑥𝑋) → ((𝑃𝐷𝑥) < 𝑅 ↔ (((𝑃𝐷𝑥) ∈ ℝ* ∧ 0 ≤ (𝑃𝐷𝑥)) ∧ (𝑃𝐷𝑥) < 𝑅)))
3728, 36bitr4id 293 . . . . . . . . . 10 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃𝑋𝑅 ∈ ℝ+) ∧ 𝑥𝑋) → (((𝑃𝐷𝑥) ∈ ℝ* ∧ 0 ≤ (𝑃𝐷𝑥) ∧ (𝑃𝐷𝑥) < 𝑅) ↔ (𝑃𝐷𝑥) < 𝑅))
3827, 37bitrd 282 . . . . . . . . 9 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃𝑋𝑅 ∈ ℝ+) ∧ 𝑥𝑋) → ((𝑃𝐷𝑥) ∈ (0[,)𝑅) ↔ (𝑃𝐷𝑥) < 𝑅))
3922, 38bitr3id 288 . . . . . . . 8 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃𝑋𝑅 ∈ ℝ+) ∧ 𝑥𝑋) → ((𝐷‘⟨𝑃, 𝑥⟩) ∈ (0[,)𝑅) ↔ (𝑃𝐷𝑥) < 𝑅))
4020, 39anbi12d 633 . . . . . . 7 (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃𝑋𝑅 ∈ ℝ+) ∧ 𝑥𝑋) → ((⟨𝑃, 𝑥⟩ ∈ (𝑋 × 𝑋) ∧ (𝐷‘⟨𝑃, 𝑥⟩) ∈ (0[,)𝑅)) ↔ (𝑥𝑋 ∧ (𝑃𝐷𝑥) < 𝑅)))
4140ex 416 . . . . . 6 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃𝑋𝑅 ∈ ℝ+) → (𝑥𝑋 → ((⟨𝑃, 𝑥⟩ ∈ (𝑋 × 𝑋) ∧ (𝐷‘⟨𝑃, 𝑥⟩) ∈ (0[,)𝑅)) ↔ (𝑥𝑋 ∧ (𝑃𝐷𝑥) < 𝑅))))
4216, 18, 41pm5.21ndd 384 . . . . 5 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃𝑋𝑅 ∈ ℝ+) → ((⟨𝑃, 𝑥⟩ ∈ (𝑋 × 𝑋) ∧ (𝐷‘⟨𝑃, 𝑥⟩) ∈ (0[,)𝑅)) ↔ (𝑥𝑋 ∧ (𝑃𝐷𝑥) < 𝑅)))
4311, 42bitrd 282 . . . 4 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃𝑋𝑅 ∈ ℝ+) → (⟨𝑃, 𝑥⟩ ∈ (𝐷 “ (0[,)𝑅)) ↔ (𝑥𝑋 ∧ (𝑃𝐷𝑥) < 𝑅)))
44 elimasng 5932 . . . . . 6 ((𝑃𝑋𝑥 ∈ V) → (𝑥 ∈ ((𝐷 “ (0[,)𝑅)) “ {𝑃}) ↔ ⟨𝑃, 𝑥⟩ ∈ (𝐷 “ (0[,)𝑅))))
4544elvd 3416 . . . . 5 (𝑃𝑋 → (𝑥 ∈ ((𝐷 “ (0[,)𝑅)) “ {𝑃}) ↔ ⟨𝑃, 𝑥⟩ ∈ (𝐷 “ (0[,)𝑅))))
46453ad2ant2 1131 . . . 4 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃𝑋𝑅 ∈ ℝ+) → (𝑥 ∈ ((𝐷 “ (0[,)𝑅)) “ {𝑃}) ↔ ⟨𝑃, 𝑥⟩ ∈ (𝐷 “ (0[,)𝑅))))
47 rabid 3296 . . . . 5 (𝑥 ∈ {𝑥𝑋 ∣ (𝑃𝐷𝑥) < 𝑅} ↔ (𝑥𝑋 ∧ (𝑃𝐷𝑥) < 𝑅))
4847a1i 11 . . . 4 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃𝑋𝑅 ∈ ℝ+) → (𝑥 ∈ {𝑥𝑋 ∣ (𝑃𝐷𝑥) < 𝑅} ↔ (𝑥𝑋 ∧ (𝑃𝐷𝑥) < 𝑅)))
4943, 46, 483bitr4d 314 . . 3 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃𝑋𝑅 ∈ ℝ+) → (𝑥 ∈ ((𝐷 “ (0[,)𝑅)) “ {𝑃}) ↔ 𝑥 ∈ {𝑥𝑋 ∣ (𝑃𝐷𝑥) < 𝑅}))
504, 5, 6, 49eqrd 3913 . 2 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃𝑋𝑅 ∈ ℝ+) → ((𝐷 “ (0[,)𝑅)) “ {𝑃}) = {𝑥𝑋 ∣ (𝑃𝐷𝑥) < 𝑅})
513, 50eqtr4d 2796 1 ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑃𝑋𝑅 ∈ ℝ+) → (𝑃(ball‘𝐷)𝑅) = ((𝐷 “ (0[,)𝑅)) “ {𝑃}))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 209   ∧ wa 399   ∧ w3a 1084   = wceq 1538   ∈ wcel 2111  {crab 3074  Vcvv 3409  {csn 4525  ⟨cop 4531   class class class wbr 5036   × cxp 5526  ◡ccnv 5527   “ cima 5531   Fn wfn 6335  ⟶wf 6336  ‘cfv 6340  (class class class)co 7156  0cc0 10588  ℝ*cxr 10725   < clt 10726   ≤ cle 10727  ℝ+crp 12443  [,)cico 12794  PsMetcpsmet 20164  ballcbl 20167 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2729  ax-sep 5173  ax-nul 5180  ax-pow 5238  ax-pr 5302  ax-un 7465  ax-cnex 10644  ax-resscn 10645  ax-1cn 10646  ax-icn 10647  ax-addcl 10648  ax-addrcl 10649  ax-mulcl 10650  ax-mulrcl 10651  ax-mulcom 10652  ax-addass 10653  ax-mulass 10654  ax-distr 10655  ax-i2m1 10656  ax-1ne0 10657  ax-1rid 10658  ax-rnegex 10659  ax-rrecex 10660  ax-cnre 10661  ax-pre-lttri 10662  ax-pre-lttrn 10663  ax-pre-ltadd 10664  ax-pre-mulgt0 10665 This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3or 1085  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2557  df-eu 2588  df-clab 2736  df-cleq 2750  df-clel 2830  df-nfc 2901  df-ne 2952  df-nel 3056  df-ral 3075  df-rex 3076  df-reu 3077  df-rmo 3078  df-rab 3079  df-v 3411  df-sbc 3699  df-csb 3808  df-dif 3863  df-un 3865  df-in 3867  df-ss 3877  df-nul 4228  df-if 4424  df-pw 4499  df-sn 4526  df-pr 4528  df-op 4532  df-uni 4802  df-iun 4888  df-br 5037  df-opab 5099  df-mpt 5117  df-id 5434  df-po 5447  df-so 5448  df-xp 5534  df-rel 5535  df-cnv 5536  df-co 5537  df-dm 5538  df-rn 5539  df-res 5540  df-ima 5541  df-iota 6299  df-fun 6342  df-fn 6343  df-f 6344  df-f1 6345  df-fo 6346  df-f1o 6347  df-fv 6348  df-riota 7114  df-ov 7159  df-oprab 7160  df-mpo 7161  df-1st 7699  df-2nd 7700  df-er 8305  df-map 8424  df-en 8541  df-dom 8542  df-sdom 8543  df-pnf 10728  df-mnf 10729  df-xr 10730  df-ltxr 10731  df-le 10732  df-sub 10923  df-neg 10924  df-div 11349  df-2 11750  df-rp 12444  df-xneg 12561  df-xadd 12562  df-xmul 12563  df-ico 12798  df-psmet 20172  df-bl 20175 This theorem is referenced by:  elbl4  23279  metustbl  23282  psmetutop  23283
 Copyright terms: Public domain W3C validator