Metamath Proof Explorer


Theorem 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 β€˜ 𝐢 ) 𝑆 ) )