Metamath Proof Explorer


Theorem blval

Description: The ball around a point P is the set of all points whose distance from P is less than the ball's radius R . (Contributed by NM, 31-Aug-2006) (Revised by Mario Carneiro, 11-Nov-2013)

Ref Expression
Assertion blval ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) = { 𝑥𝑋 ∣ ( 𝑃 𝐷 𝑥 ) < 𝑅 } )

Proof

Step Hyp Ref Expression
1 blfval ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( ball ‘ 𝐷 ) = ( 𝑦𝑋 , 𝑟 ∈ ℝ* ↦ { 𝑥𝑋 ∣ ( 𝑦 𝐷 𝑥 ) < 𝑟 } ) )
2 1 3ad2ant1 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) → ( ball ‘ 𝐷 ) = ( 𝑦𝑋 , 𝑟 ∈ ℝ* ↦ { 𝑥𝑋 ∣ ( 𝑦 𝐷 𝑥 ) < 𝑟 } ) )
3 simprl ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) ∧ ( 𝑦 = 𝑃𝑟 = 𝑅 ) ) → 𝑦 = 𝑃 )
4 3 oveq1d ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) ∧ ( 𝑦 = 𝑃𝑟 = 𝑅 ) ) → ( 𝑦 𝐷 𝑥 ) = ( 𝑃 𝐷 𝑥 ) )
5 simprr ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) ∧ ( 𝑦 = 𝑃𝑟 = 𝑅 ) ) → 𝑟 = 𝑅 )
6 4 5 breq12d ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) ∧ ( 𝑦 = 𝑃𝑟 = 𝑅 ) ) → ( ( 𝑦 𝐷 𝑥 ) < 𝑟 ↔ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) )
7 6 rabbidv ( ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) ∧ ( 𝑦 = 𝑃𝑟 = 𝑅 ) ) → { 𝑥𝑋 ∣ ( 𝑦 𝐷 𝑥 ) < 𝑟 } = { 𝑥𝑋 ∣ ( 𝑃 𝐷 𝑥 ) < 𝑅 } )
8 simp2 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) → 𝑃𝑋 )
9 simp3 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) → 𝑅 ∈ ℝ* )
10 elfvdm ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 ∈ dom ∞Met )
11 10 3ad2ant1 ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) → 𝑋 ∈ dom ∞Met )
12 rabexg ( 𝑋 ∈ dom ∞Met → { 𝑥𝑋 ∣ ( 𝑃 𝐷 𝑥 ) < 𝑅 } ∈ V )
13 11 12 syl ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) → { 𝑥𝑋 ∣ ( 𝑃 𝐷 𝑥 ) < 𝑅 } ∈ V )
14 2 7 8 9 13 ovmpod ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃𝑋𝑅 ∈ ℝ* ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) = { 𝑥𝑋 ∣ ( 𝑃 𝐷 𝑥 ) < 𝑅 } )