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	syl5eq	⊢ ( ( 𝑃 ∈ 𝑌 ∧ 𝑥 ∈ 𝑌 ) → ( 𝑃 𝐶 𝑥 ) = ( 𝑃 𝐷 𝑥 ) )
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 ‘ 𝐷 ) 𝑅 ) ∩ 𝑌 ) )