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 syl5bb ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ ( 𝑋𝑌 ) ∧ 𝑅 ∈ ℝ* ) → ( 𝑥 ∈ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ 𝑌 ) ↔ ( ( 𝑥𝑋 ∧ ( 𝑃 𝐷 𝑥 ) < 𝑅 ) ∧ 𝑥𝑌 ) ) )
28 17 21 27 3bitr4d ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ ( 𝑋𝑌 ) ∧ 𝑅 ∈ ℝ* ) → ( 𝑥 ∈ ( 𝑃 ( ball ‘ 𝐶 ) 𝑅 ) ↔ 𝑥 ∈ ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ 𝑌 ) ) )
29 28 eqrdv ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ ( 𝑋𝑌 ) ∧ 𝑅 ∈ ℝ* ) → ( 𝑃 ( ball ‘ 𝐶 ) 𝑅 ) = ( ( 𝑃 ( ball ‘ 𝐷 ) 𝑅 ) ∩ 𝑌 ) )