Step |
Hyp |
Ref |
Expression |
1 |
|
blssp.2 |
⊢ 𝑁 = ( 𝑀 ↾ ( 𝑆 × 𝑆 ) ) |
2 |
|
metxmet |
⊢ ( 𝑀 ∈ ( Met ‘ 𝑋 ) → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ) |
3 |
2
|
ad2antrr |
⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑌 ∈ 𝑆 ∧ 𝑅 ∈ ℝ+ ) ) → 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ) |
4 |
|
simprl |
⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑌 ∈ 𝑆 ∧ 𝑅 ∈ ℝ+ ) ) → 𝑌 ∈ 𝑆 ) |
5 |
|
simplr |
⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑌 ∈ 𝑆 ∧ 𝑅 ∈ ℝ+ ) ) → 𝑆 ⊆ 𝑋 ) |
6 |
|
sseqin2 |
⊢ ( 𝑆 ⊆ 𝑋 ↔ ( 𝑋 ∩ 𝑆 ) = 𝑆 ) |
7 |
5 6
|
sylib |
⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑌 ∈ 𝑆 ∧ 𝑅 ∈ ℝ+ ) ) → ( 𝑋 ∩ 𝑆 ) = 𝑆 ) |
8 |
4 7
|
eleqtrrd |
⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑌 ∈ 𝑆 ∧ 𝑅 ∈ ℝ+ ) ) → 𝑌 ∈ ( 𝑋 ∩ 𝑆 ) ) |
9 |
|
rpxr |
⊢ ( 𝑅 ∈ ℝ+ → 𝑅 ∈ ℝ* ) |
10 |
9
|
ad2antll |
⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑌 ∈ 𝑆 ∧ 𝑅 ∈ ℝ+ ) ) → 𝑅 ∈ ℝ* ) |
11 |
1
|
blres |
⊢ ( ( 𝑀 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑌 ∈ ( 𝑋 ∩ 𝑆 ) ∧ 𝑅 ∈ ℝ* ) → ( 𝑌 ( ball ‘ 𝑁 ) 𝑅 ) = ( ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ∩ 𝑆 ) ) |
12 |
3 8 10 11
|
syl3anc |
⊢ ( ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑆 ⊆ 𝑋 ) ∧ ( 𝑌 ∈ 𝑆 ∧ 𝑅 ∈ ℝ+ ) ) → ( 𝑌 ( ball ‘ 𝑁 ) 𝑅 ) = ( ( 𝑌 ( ball ‘ 𝑀 ) 𝑅 ) ∩ 𝑆 ) ) |