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

Metamath Proof Explorer

Theorem blres

Description: A ball in a restricted metric space. (Contributed by Mario Carneiro, 5-Jan-2014)

Ref Expression
Hypothesis blres.2 ⊢ 𝐶 = ( 𝐷 ↾ ( 𝑌 × 𝑌 ) )
Assertion blres ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ ( 𝑋 ∩ 𝑌 ) ∧ 𝑅 ∈ ℝ* ) → ( 𝑃 ( ball ‘ 𝐶 ) 𝑅 ) = ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ 𝑌 ) )

Proof

Step Hyp Ref Expression
1 blres.2 ⊢ 𝐶 = ( 𝐷 ↾ ( 𝑌 × 𝑌 ) )
2 elinel2 ⊢ ( 𝑃 ∈ ( 𝑋 ∩ 𝑌 ) → 𝑃 ∈ 𝑌 )
3 1 oveqi ⊢ ( 𝑃 𝐶 𝑥 ) = ( 𝑃 ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) 𝑥 )
4 ovres ⊢ ( ( 𝑃 ∈ 𝑌 ∧ 𝑥 ∈ 𝑌 ) → ( 𝑃 ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) 𝑥 ) = ( 𝑃 𝐷 𝑥 ) )
5 3 4 eqtrid ⊢ ( ( 𝑃 ∈ 𝑌 ∧ 𝑥 ∈ 𝑌 ) → ( 𝑃 𝐶 𝑥 ) = ( 𝑃 𝐷 𝑥 ) )
6 2 5 sylan ⊢ ( ( 𝑃 ∈ ( 𝑋 ∩ 𝑌 ) ∧ 𝑥 ∈ 𝑌 ) → ( 𝑃 𝐶 𝑥 ) = ( 𝑃 𝐷 𝑥 ) )
7 6 breq1d ⊢ ( ( 𝑃 ∈ ( 𝑋 ∩ 𝑌 ) ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝑃 𝐶 𝑥 ) < 𝑅 ↔ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) )
8 7 anbi2d ⊢ ( ( 𝑃 ∈ ( 𝑋 ∩ 𝑌 ) ∧ 𝑥 ∈ 𝑌 ) → ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐶 𝑥 ) < 𝑅 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) )
9 8 pm5.32da ⊢ ( 𝑃 ∈ ( 𝑋 ∩ 𝑌 ) → ( ( 𝑥 ∈ 𝑌 ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐶 𝑥 ) < 𝑅 ) ) ↔ ( 𝑥 ∈ 𝑌 ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) ) )
10 9 3ad2ant2 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ ( 𝑋 ∩ 𝑌 ) ∧ 𝑅 ∈ ℝ* ) → ( ( 𝑥 ∈ 𝑌 ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐶 𝑥 ) < 𝑅 ) ) ↔ ( 𝑥 ∈ 𝑌 ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) ) )
11 elin ⊢ ( 𝑥 ∈ ( 𝑋 ∩ 𝑌 ) ↔ ( 𝑥 ∈ 𝑋 ∧ 𝑥 ∈ 𝑌 ) )
12 11 biancomi ⊢ ( 𝑥 ∈ ( 𝑋 ∩ 𝑌 ) ↔ ( 𝑥 ∈ 𝑌 ∧ 𝑥 ∈ 𝑋 ) )
13 12 anbi1i ⊢ ( ( 𝑥 ∈ ( 𝑋 ∩ 𝑌 ) ∧ ( 𝑃 𝐶 𝑥 ) < 𝑅 ) ↔ ( ( 𝑥 ∈ 𝑌 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑃 𝐶 𝑥 ) < 𝑅 ) )
14 anass ⊢ ( ( ( 𝑥 ∈ 𝑌 ∧ 𝑥 ∈ 𝑋 ) ∧ ( 𝑃 𝐶 𝑥 ) < 𝑅 ) ↔ ( 𝑥 ∈ 𝑌 ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐶 𝑥 ) < 𝑅 ) ) )
15 13 14 bitri ⊢ ( ( 𝑥 ∈ ( 𝑋 ∩ 𝑌 ) ∧ ( 𝑃 𝐶 𝑥 ) < 𝑅 ) ↔ ( 𝑥 ∈ 𝑌 ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐶 𝑥 ) < 𝑅 ) ) )
16 ancom ⊢ ( ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ∧ 𝑥 ∈ 𝑌 ) ↔ ( 𝑥 ∈ 𝑌 ∧ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) )
17 10 15 16 3bitr4g ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ ( 𝑋 ∩ 𝑌 ) ∧ 𝑅 ∈ ℝ* ) → ( ( 𝑥 ∈ ( 𝑋 ∩ 𝑌 ) ∧ ( 𝑃 𝐶 𝑥 ) < 𝑅 ) ↔ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ∧ 𝑥 ∈ 𝑌 ) ) )
18 xmetres ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝐷 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( ∞Met ‘ ( 𝑋 ∩ 𝑌 ) ) )
19 1 18 eqeltrid ⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐶 ∈ ( ∞Met ‘ ( 𝑋 ∩ 𝑌 ) ) )
20 elbl ⊢ ( ( 𝐶 ∈ ( ∞Met ‘ ( 𝑋 ∩ 𝑌 ) ) ∧ 𝑃 ∈ ( 𝑋 ∩ 𝑌 ) ∧ 𝑅 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐶 ) 𝑅 ) ↔ ( 𝑥 ∈ ( 𝑋 ∩ 𝑌 ) ∧ ( 𝑃 𝐶 𝑥 ) < 𝑅 ) ) )
21 19 20 syl3an1 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ ( 𝑋 ∩ 𝑌 ) ∧ 𝑅 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐶 ) 𝑅 ) ↔ ( 𝑥 ∈ ( 𝑋 ∩ 𝑌 ) ∧ ( 𝑃 𝐶 𝑥 ) < 𝑅 ) ) )
22 elin ⊢ ( 𝑥 ∈ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ 𝑌 ) ↔ ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∧ 𝑥 ∈ 𝑌 ) )
23 elinel1 ⊢ ( 𝑃 ∈ ( 𝑋 ∩ 𝑌 ) → 𝑃 ∈ 𝑋 )
24 elbl ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑅 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) )
25 23 24 syl3an2 ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ ( 𝑋 ∩ 𝑌 ) ∧ 𝑅 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ↔ ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ) )
26 25 anbi1d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ ( 𝑋 ∩ 𝑌 ) ∧ 𝑅 ∈ ℝ* ) → ( ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∧ 𝑥 ∈ 𝑌 ) ↔ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ∧ 𝑥 ∈ 𝑌 ) ) )
27 22 26 bitrid ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ ( 𝑋 ∩ 𝑌 ) ∧ 𝑅 ∈ ℝ* ) → ( 𝑥 ∈ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ 𝑌 ) ↔ ( ( 𝑥 ∈ 𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ∧ 𝑥 ∈ 𝑌 ) ) )
28 17 21 27 3bitr4d ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ ( 𝑋 ∩ 𝑌 ) ∧ 𝑅 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐶 ) 𝑅 ) ↔ 𝑥 ∈ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ 𝑌 ) ) )
29 28 eqrdv ⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ ( 𝑋 ∩ 𝑌 ) ∧ 𝑅 ∈ ℝ* ) → ( 𝑃 ( ball ‘ 𝐶 ) 𝑅 ) = ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ 𝑌 ) )