This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem elbl4

Description: Membership in a ball, alternative definition. (Contributed by Thierry Arnoux, 26-Jan-2018) (Revised by Thierry Arnoux, 11-Mar-2018)

Ref Expression
Assertion elbl4 ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐵 ∈ ( 𝐴 ( ball ‘ 𝐷 ) 𝑅 ) ↔ 𝐵 ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) 𝐴 ) )

Proof

Step Hyp Ref Expression
1 rpxr ⊢ ( 𝑅 ∈ ℝ+ → 𝑅 ∈ ℝ* )
2 blcomps ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ* ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐵 ∈ ( 𝐴 ( ball ‘ 𝐷 ) 𝑅 ) ↔ 𝐴 ∈ ( 𝐵 ( ball ‘ 𝐷 ) 𝑅 ) ) )
3 1 2 sylanl2 ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐵 ∈ ( 𝐴 ( ball ‘ 𝐷 ) 𝑅 ) ↔ 𝐴 ∈ ( 𝐵 ( ball ‘ 𝐷 ) 𝑅 ) ) )
4 simpll ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐷 ∈ ( PsMet ‘ 𝑋 ) )
5 simprr ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝐵 ∈ 𝑋 )
6 simplr ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → 𝑅 ∈ ℝ+ )
7 blval2 ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐵 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) → ( 𝐵 ( ball ‘ 𝐷 ) 𝑅 ) = ( ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) “ { 𝐵 } ) )
8 7 eleq2d ⊢ ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝐵 ∈ 𝑋 ∧ 𝑅 ∈ ℝ+ ) → ( 𝐴 ∈ ( 𝐵 ( ball ‘ 𝐷 ) 𝑅 ) ↔ 𝐴 ∈ ( ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) “ { 𝐵 } ) ) )
9 4 5 6 8 syl3anc ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 ∈ ( 𝐵 ( ball ‘ 𝐷 ) 𝑅 ) ↔ 𝐴 ∈ ( ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) “ { 𝐵 } ) ) )
10 elimasng ⊢ ( ( 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ∈ ( ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) “ { 𝐵 } ) ↔ ⟨ 𝐵 , 𝐴 ⟩ ∈ ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) ) )
11 df-br ⊢ ( 𝐵 ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) 𝐴 ↔ ⟨ 𝐵 , 𝐴 ⟩ ∈ ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) )
12 10 11 bitr4di ⊢ ( ( 𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ) → ( 𝐴 ∈ ( ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) “ { 𝐵 } ) ↔ 𝐵 ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) 𝐴 ) )
13 12 ancoms ⊢ ( ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐴 ∈ ( ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) “ { 𝐵 } ) ↔ 𝐵 ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) 𝐴 ) )
14 13 adantl ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐴 ∈ ( ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) “ { 𝐵 } ) ↔ 𝐵 ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) 𝐴 ) )
15 3 9 14 3bitrd ⊢ ( ( ( 𝐷 ∈ ( PsMet ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ+ ) ∧ ( 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) ) → ( 𝐵 ∈ ( 𝐴 ( ball ‘ 𝐷 ) 𝑅 ) ↔ 𝐵 ( ◡ 𝐷 “ ( 0 [,) 𝑅 ) ) 𝐴 ) )