Metamath Proof Explorer

Theorem blval2

Description: The ball around a point P , alternative definition. (Contributed by Thierry Arnoux, 7-Dec-2017) (Revised by Thierry Arnoux, 11-Mar-2018)

Ref Expression
Assertion blval2 ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) = ( ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) “ { 𝑃 } ) )

Proof

Step Hyp Ref Expression
1 rpxr ⊢ ( 𝑅 ∈ ℝ+ → 𝑅 ∈ ℝ* )
2 blvalps ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) = { 𝑥 ∈ 𝑋 ∣ ( 𝑃 𝐷 𝑥 ) < 𝑅 } )
3 1 2 syl3an3 ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) = { 𝑥 ∈ 𝑋 ∣ ( 𝑃 𝐷 𝑥 ) < 𝑅 } )
4 nfv ⊢ Ⅎ 𝑥 ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ )
5 nfcv ⊢ Ⅎ 𝑥 ( ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) “ { 𝑃 } )
6 nfrab1 ⊢ Ⅎ 𝑥 { 𝑥 ∈ 𝑋 ∣ ( 𝑃 𝐷 𝑥 ) < 𝑅 }
7 psmetf ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* )
8 ffn ⊢ ( 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ* → 𝐷 Fn ( 𝑋 × 𝑋 ) )
9 elpreima ⊢ ( 𝐷 Fn ( 𝑋 × 𝑋 ) → ( ⟨ 𝑃 , 𝑥 ⟩ ∈ ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) ↔ ( ⟨ 𝑃 , 𝑥 ⟩ ∈ ( 𝑋 × 𝑋 ) ∧ ( 𝐷 ‘ ⟨ 𝑃 , 𝑥 ⟩ ) ∈ ( 0 [,) 𝑅 ) ) ) )
10 7 8 9 3syl ⊢ ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) → ( ⟨ 𝑃 , 𝑥 ⟩ ∈ ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) ↔ ( ⟨ 𝑃 , 𝑥 ⟩ ∈ ( 𝑋 × 𝑋 ) ∧ ( 𝐷 ‘ ⟨ 𝑃 , 𝑥 ⟩ ) ∈ ( 0 [,) 𝑅 ) ) ) )
11 10 3ad2ant1 ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) → ( ⟨ 𝑃 , 𝑥 ⟩ ∈ ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) ↔ ( ⟨ 𝑃 , 𝑥 ⟩ ∈ ( 𝑋 × 𝑋 ) ∧ ( 𝐷 ‘ ⟨ 𝑃 , 𝑥 ⟩ ) ∈ ( 0 [,) 𝑅 ) ) ) )
12 opelxp ⊢ ( ⟨ 𝑃 , 𝑥 ⟩ ∈ ( 𝑋 × 𝑋 ) ↔ ( 𝑃 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) )
13 12 baib ⊢ ( 𝑃 ∈ 𝑋 → ( ⟨ 𝑃 , 𝑥 ⟩ ∈ ( 𝑋 × 𝑋 ) ↔ 𝑥 ∈ 𝑋 ) )
14 13 3ad2ant2 ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) → ( ⟨ 𝑃 , 𝑥 ⟩ ∈ ( 𝑋 × 𝑋 ) ↔ 𝑥 ∈ 𝑋 ) )
15 14 biimpd ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) → ( ⟨ 𝑃 , 𝑥 ⟩ ∈ ( 𝑋 × 𝑋 ) → 𝑥 ∈ 𝑋 ) )
16 15 adantrd ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) → ( ( ⟨ 𝑃 , 𝑥 ⟩ ∈ ( 𝑋 × 𝑋 ) ∧ ( 𝐷 ‘ ⟨ 𝑃 , 𝑥 ⟩ ) ∈ ( 0 [,) 𝑅 ) ) → 𝑥 ∈ 𝑋 ) )
17 simprl ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) → 𝑥 ∈ 𝑋 )
18 17 ex ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) → ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) → 𝑥 ∈ 𝑋 ) )
19 simpl2 ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) → 𝑃 ∈ 𝑋 )
20 19 13 syl ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) → ( ⟨ 𝑃 , 𝑥 ⟩ ∈ ( 𝑋 × 𝑋 ) ↔ 𝑥 ∈ 𝑋 ) )
21 df-ov ⊢ ( 𝑃 𝐷 𝑥 ) = ( 𝐷 ‘ ⟨ 𝑃 , 𝑥 ⟩ )
22 21 eleq1i ⊢ ( ( 𝑃 𝐷 𝑥 ) ∈ ( 0 [,) 𝑅 ) ↔ ( 𝐷 ‘ ⟨ 𝑃 , 𝑥 ⟩ ) ∈ ( 0 [,) 𝑅 ) )
23 0xr ⊢ 0 ∈ ℝ*
24 simpl3 ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) → 𝑅 ∈ ℝ+ )
25 24 rpxrd ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) → 𝑅 ∈ ℝ* )
26 elico1 ⊢ ( ( 0 ∈ ℝ* ∧ 𝑅 ∈ ℝ* ) → ( ( 𝑃 𝐷 𝑥 ) ∈ ( 0 [,) 𝑅 ) ↔ ( ( 𝑃 𝐷 𝑥 ) ∈ ℝ* ∧ 0 ≤ ( 𝑃 𝐷 𝑥 ) ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) )
27 23 25 26 sylancr ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑃 𝐷 𝑥 ) ∈ ( 0 [,) 𝑅 ) ↔ ( ( 𝑃 𝐷 𝑥 ) ∈ ℝ* ∧ 0 ≤ ( 𝑃 𝐷 𝑥 ) ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) )
28 df-3an ⊢ ( ( ( 𝑃 𝐷 𝑥 ) ∈ ℝ* ∧ 0 ≤ ( 𝑃 𝐷 𝑥 ) ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ↔ ( ( ( 𝑃 𝐷 𝑥 ) ∈ ℝ* ∧ 0 ≤ ( 𝑃 𝐷 𝑥 ) ) ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) )
29 simpl1 ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
30 simpr ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) → 𝑥 ∈ 𝑋 )
31 psmetcl ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑥 ) ∈ ℝ* )
32 29 19 30 31 syl3anc ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑥 ) ∈ ℝ* )
33 psmetge0 ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑥 ∈ 𝑋 ) → 0 ≤ ( 𝑃 𝐷 𝑥 ) )
34 29 19 30 33 syl3anc ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) → 0 ≤ ( 𝑃 𝐷 𝑥 ) )
35 32 34 jca ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑃 𝐷 𝑥 ) ∈ ℝ* ∧ 0 ≤ ( 𝑃 𝐷 𝑥 ) ) )
36 35 biantrurd ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑃 𝐷 𝑥 ) < 𝑅 ↔ ( ( ( 𝑃 𝐷 𝑥 ) ∈ ℝ* ∧ 0 ≤ ( 𝑃 𝐷 𝑥 ) ) ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) )
37 28 36 bitr4id ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ( 𝑃 𝐷 𝑥 ) ∈ ℝ* ∧ 0 ≤ ( 𝑃 𝐷 𝑥 ) ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ↔ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) )
38 27 37 bitrd ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝑃 𝐷 𝑥 ) ∈ ( 0 [,) 𝑅 ) ↔ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) )
39 22 38 bitr3id ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) → ( ( 𝐷 ‘ ⟨ 𝑃 , 𝑥 ⟩ ) ∈ ( 0 [,) 𝑅 ) ↔ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) )
40 20 39 anbi12d ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) ∧ 𝑥 ∈ 𝑋 ) → ( ( ⟨ 𝑃 , 𝑥 ⟩ ∈ ( 𝑋 × 𝑋 ) ∧ ( 𝐷 ‘ ⟨ 𝑃 , 𝑥 ⟩ ) ∈ ( 0 [,) 𝑅 ) ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) )
41 40 ex ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) → ( 𝑥 ∈ 𝑋 → ( ( ⟨ 𝑃 , 𝑥 ⟩ ∈ ( 𝑋 × 𝑋 ) ∧ ( 𝐷 ‘ ⟨ 𝑃 , 𝑥 ⟩ ) ∈ ( 0 [,) 𝑅 ) ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) ) )
42 16 18 41 pm5.21ndd ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) → ( ( ⟨ 𝑃 , 𝑥 ⟩ ∈ ( 𝑋 × 𝑋 ) ∧ ( 𝐷 ‘ ⟨ 𝑃 , 𝑥 ⟩ ) ∈ ( 0 [,) 𝑅 ) ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) )
43 11 42 bitrd ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) → ( ⟨ 𝑃 , 𝑥 ⟩ ∈ ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) )
44 elimasng ⊢ ( ( 𝑃 ∈ 𝑋 ∧ 𝑥 ∈ V ) → ( 𝑥 ∈ ( ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) “ { 𝑃 } ) ↔ ⟨ 𝑃 , 𝑥 ⟩ ∈ ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) ) )
45 44 elvd ⊢ ( 𝑃 ∈ 𝑋 → ( 𝑥 ∈ ( ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) “ { 𝑃 } ) ↔ ⟨ 𝑃 , 𝑥 ⟩ ∈ ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) ) )
46 45 3ad2ant2 ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) → ( 𝑥 ∈ ( ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) “ { 𝑃 } ) ↔ ⟨ 𝑃 , 𝑥 ⟩ ∈ ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) ) )
47 rabid ⊢ ( 𝑥 ∈ { 𝑥 ∈ 𝑋 ∣ ( 𝑃 𝐷 𝑥 ) < 𝑅 } ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) )
48 47 a1i ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) → ( 𝑥 ∈ { 𝑥 ∈ 𝑋 ∣ ( 𝑃 𝐷 𝑥 ) < 𝑅 } ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) )
49 43 46 48 3bitr4d ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) → ( 𝑥 ∈ ( ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) “ { 𝑃 } ) ↔ 𝑥 ∈ { 𝑥 ∈ 𝑋 ∣ ( 𝑃 𝐷 𝑥 ) < 𝑅 } ) )
50 4 5 6 49 eqrd ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) → ( ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) “ { 𝑃 } ) = { 𝑥 ∈ 𝑋 ∣ ( 𝑃 𝐷 𝑥 ) < 𝑅 } )
51 3 50 eqtr4d ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) = ( ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) “ { 𝑃 } ) )