stdbdbl

Description: The standard bounded metric corresponding to C generates the same balls as C for radii less than R . (Contributed by Mario Carneiro, 26-Aug-2015)

		Ref	Expression
	Hypothesis	stdbdmet.1	⊢ 𝐷 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ if ( ( 𝑥 𝐶 𝑦 ) ≤ 𝑅 , ( 𝑥 𝐶 𝑦 ) , 𝑅 ) )
	Assertion	stdbdbl	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ^* ∧ 𝑆 ≤ 𝑅 ) ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) = ( 𝑃 ( ball ‘ 𝐶 ) 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		stdbdmet.1	⊢ 𝐷 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ if ( ( 𝑥 𝐶 𝑦 ) ≤ 𝑅 , ( 𝑥 𝐶 𝑦 ) , 𝑅 ) )
2		simpll2	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ^* ∧ 𝑆 ≤ 𝑅 ) ) ∧ 𝑧 ∈ 𝑋 ) → 𝑅 ∈ ℝ^* )
3		simpr1	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ^* ∧ 𝑆 ≤ 𝑅 ) ) → 𝑃 ∈ 𝑋 )
4	3	adantr	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ^* ∧ 𝑆 ≤ 𝑅 ) ) ∧ 𝑧 ∈ 𝑋 ) → 𝑃 ∈ 𝑋 )
5		simpr	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ^* ∧ 𝑆 ≤ 𝑅 ) ) ∧ 𝑧 ∈ 𝑋 ) → 𝑧 ∈ 𝑋 )
6	1	stdbdmetval	⊢ ( ( 𝑅 ∈ ℝ^* ∧ 𝑃 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑧 ) = if ( ( 𝑃 𝐶 𝑧 ) ≤ 𝑅 , ( 𝑃 𝐶 𝑧 ) , 𝑅 ) )
7	2 4 5 6	syl3anc	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ^* ∧ 𝑆 ≤ 𝑅 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑃 𝐷 𝑧 ) = if ( ( 𝑃 𝐶 𝑧 ) ≤ 𝑅 , ( 𝑃 𝐶 𝑧 ) , 𝑅 ) )
8	7	breq1d	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ^* ∧ 𝑆 ≤ 𝑅 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝑃 𝐷 𝑧 ) < 𝑆 ↔ if ( ( 𝑃 𝐶 𝑧 ) ≤ 𝑅 , ( 𝑃 𝐶 𝑧 ) , 𝑅 ) < 𝑆 ) )
9		simplr3	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ^* ∧ 𝑆 ≤ 𝑅 ) ) ∧ 𝑧 ∈ 𝑋 ) → 𝑆 ≤ 𝑅 )
10	9	biantrud	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ^* ∧ 𝑆 ≤ 𝑅 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑆 ≤ ( 𝑃 𝐶 𝑧 ) ↔ ( 𝑆 ≤ ( 𝑃 𝐶 𝑧 ) ∧ 𝑆 ≤ 𝑅 ) ) )
11		simpr2	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ^* ∧ 𝑆 ≤ 𝑅 ) ) → 𝑆 ∈ ℝ^* )
12	11	adantr	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ^* ∧ 𝑆 ≤ 𝑅 ) ) ∧ 𝑧 ∈ 𝑋 ) → 𝑆 ∈ ℝ^* )
13		simpl1	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ^* ∧ 𝑆 ≤ 𝑅 ) ) → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
14	13	adantr	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ^* ∧ 𝑆 ≤ 𝑅 ) ) ∧ 𝑧 ∈ 𝑋 ) → 𝐶 ∈ ( ∞Met ‘ 𝑋 ) )
15		xmetcl	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑧 ∈ 𝑋 ) → ( 𝑃 𝐶 𝑧 ) ∈ ℝ^* )
16	14 4 5 15	syl3anc	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ^* ∧ 𝑆 ≤ 𝑅 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑃 𝐶 𝑧 ) ∈ ℝ^* )
17		xrlemin	⊢ ( ( 𝑆 ∈ ℝ^* ∧ ( 𝑃 𝐶 𝑧 ) ∈ ℝ^* ∧ 𝑅 ∈ ℝ^* ) → ( 𝑆 ≤ if ( ( 𝑃 𝐶 𝑧 ) ≤ 𝑅 , ( 𝑃 𝐶 𝑧 ) , 𝑅 ) ↔ ( 𝑆 ≤ ( 𝑃 𝐶 𝑧 ) ∧ 𝑆 ≤ 𝑅 ) ) )
18	12 16 2 17	syl3anc	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ^* ∧ 𝑆 ≤ 𝑅 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑆 ≤ if ( ( 𝑃 𝐶 𝑧 ) ≤ 𝑅 , ( 𝑃 𝐶 𝑧 ) , 𝑅 ) ↔ ( 𝑆 ≤ ( 𝑃 𝐶 𝑧 ) ∧ 𝑆 ≤ 𝑅 ) ) )
19	10 18	bitr4d	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ^* ∧ 𝑆 ≤ 𝑅 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( 𝑆 ≤ ( 𝑃 𝐶 𝑧 ) ↔ 𝑆 ≤ if ( ( 𝑃 𝐶 𝑧 ) ≤ 𝑅 , ( 𝑃 𝐶 𝑧 ) , 𝑅 ) ) )
20	19	notbid	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ^* ∧ 𝑆 ≤ 𝑅 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ¬ 𝑆 ≤ ( 𝑃 𝐶 𝑧 ) ↔ ¬ 𝑆 ≤ if ( ( 𝑃 𝐶 𝑧 ) ≤ 𝑅 , ( 𝑃 𝐶 𝑧 ) , 𝑅 ) ) )
21		xrltnle	⊢ ( ( ( 𝑃 𝐶 𝑧 ) ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ) → ( ( 𝑃 𝐶 𝑧 ) < 𝑆 ↔ ¬ 𝑆 ≤ ( 𝑃 𝐶 𝑧 ) ) )
22	16 12 21	syl2anc	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ^* ∧ 𝑆 ≤ 𝑅 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝑃 𝐶 𝑧 ) < 𝑆 ↔ ¬ 𝑆 ≤ ( 𝑃 𝐶 𝑧 ) ) )
23	16 2	ifcld	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ^* ∧ 𝑆 ≤ 𝑅 ) ) ∧ 𝑧 ∈ 𝑋 ) → if ( ( 𝑃 𝐶 𝑧 ) ≤ 𝑅 , ( 𝑃 𝐶 𝑧 ) , 𝑅 ) ∈ ℝ^* )
24		xrltnle	⊢ ( ( if ( ( 𝑃 𝐶 𝑧 ) ≤ 𝑅 , ( 𝑃 𝐶 𝑧 ) , 𝑅 ) ∈ ℝ^* ∧ 𝑆 ∈ ℝ^* ) → ( if ( ( 𝑃 𝐶 𝑧 ) ≤ 𝑅 , ( 𝑃 𝐶 𝑧 ) , 𝑅 ) < 𝑆 ↔ ¬ 𝑆 ≤ if ( ( 𝑃 𝐶 𝑧 ) ≤ 𝑅 , ( 𝑃 𝐶 𝑧 ) , 𝑅 ) ) )
25	23 12 24	syl2anc	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ^* ∧ 𝑆 ≤ 𝑅 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( if ( ( 𝑃 𝐶 𝑧 ) ≤ 𝑅 , ( 𝑃 𝐶 𝑧 ) , 𝑅 ) < 𝑆 ↔ ¬ 𝑆 ≤ if ( ( 𝑃 𝐶 𝑧 ) ≤ 𝑅 , ( 𝑃 𝐶 𝑧 ) , 𝑅 ) ) )
26	20 22 25	3bitr4d	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ^* ∧ 𝑆 ≤ 𝑅 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝑃 𝐶 𝑧 ) < 𝑆 ↔ if ( ( 𝑃 𝐶 𝑧 ) ≤ 𝑅 , ( 𝑃 𝐶 𝑧 ) , 𝑅 ) < 𝑆 ) )
27	8 26	bitr4d	⊢ ( ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ^* ∧ 𝑆 ≤ 𝑅 ) ) ∧ 𝑧 ∈ 𝑋 ) → ( ( 𝑃 𝐷 𝑧 ) < 𝑆 ↔ ( 𝑃 𝐶 𝑧 ) < 𝑆 ) )
28	27	rabbidva	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ^* ∧ 𝑆 ≤ 𝑅 ) ) → { 𝑧 ∈ 𝑋 ∣ ( 𝑃 𝐷 𝑧 ) < 𝑆 } = { 𝑧 ∈ 𝑋 ∣ ( 𝑃 𝐶 𝑧 ) < 𝑆 } )
29	1	stdbdxmet	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
30	29	adantr	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ^* ∧ 𝑆 ≤ 𝑅 ) ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
31		blval	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ^* ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) = { 𝑧 ∈ 𝑋 ∣ ( 𝑃 𝐷 𝑧 ) < 𝑆 } )
32	30 3 11 31	syl3anc	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ^* ∧ 𝑆 ≤ 𝑅 ) ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) = { 𝑧 ∈ 𝑋 ∣ ( 𝑃 𝐷 𝑧 ) < 𝑆 } )
33		blval	⊢ ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ^* ) → ( 𝑃 ( ball ‘ 𝐶 ) 𝑆 ) = { 𝑧 ∈ 𝑋 ∣ ( 𝑃 𝐶 𝑧 ) < 𝑆 } )
34	13 3 11 33	syl3anc	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ^* ∧ 𝑆 ≤ 𝑅 ) ) → ( 𝑃 ( ball ‘ 𝐶 ) 𝑆 ) = { 𝑧 ∈ 𝑋 ∣ ( 𝑃 𝐶 𝑧 ) < 𝑆 } )
35	28 32 34	3eqtr4d	⊢ ( ( ( 𝐶 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑅 ∈ ℝ^* ∧ 0 < 𝑅 ) ∧ ( 𝑃 ∈ 𝑋 ∧ 𝑆 ∈ ℝ^* ∧ 𝑆 ≤ 𝑅 ) ) → ( 𝑃 ( ball ‘ 𝐷 ) 𝑆 ) = ( 𝑃 ( ball ‘ 𝐶 ) 𝑆 ) )

Metamath Proof Explorer

Theorem stdbdbl

Proof