Metamath Proof Explorer

Theorem equivbnd2

Description: If balls are totally bounded in the metric M , then balls are totally bounded in the equivalent metric N . (Contributed by Mario Carneiro, 15-Sep-2015)

Ref Expression
Hypotheses equivbnd2.1 ⊢ ( 𝜑 → 𝑀 ∈ ( Met ‘ 𝑋 ) )
equivbnd2.2 ⊢ ( 𝜑 → 𝑁 ∈ ( Met ‘ 𝑋 ) )
equivbnd2.3 ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
equivbnd2.4 ⊢ ( 𝜑 → 𝑆 ∈ ℝ+ )
equivbnd2.5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝑁 𝑦 ) ≤ ( 𝑅 · ( 𝑥 𝑀 𝑦 ) ) )
equivbnd2.6 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝑀 𝑦 ) ≤ ( 𝑆 · ( 𝑥 𝑁 𝑦 ) ) )
equivbnd2.7 ⊢ 𝐶 = ( 𝑀 ↾ ( 𝑌 × 𝑌 ) )
equivbnd2.8 ⊢ 𝐷 = ( 𝑁 ↾ ( 𝑌 × 𝑌 ) )
equivbnd2.9 ⊢ ( 𝜑 → ( 𝐶 ∈ ( TotBnd ‘ 𝑌 ) ↔ 𝐶 ∈ ( Bnd ‘ 𝑌 ) ) )
Assertion equivbnd2 ( 𝜑 → ( 𝐷 ∈ ( TotBnd ‘ 𝑌 ) ↔ 𝐷 ∈ ( Bnd ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 equivbnd2.1 ⊢ ( 𝜑 → 𝑀 ∈ ( Met ‘ 𝑋 ) )
2 equivbnd2.2 ⊢ ( 𝜑 → 𝑁 ∈ ( Met ‘ 𝑋 ) )
3 equivbnd2.3 ⊢ ( 𝜑 → 𝑅 ∈ ℝ+ )
4 equivbnd2.4 ⊢ ( 𝜑 → 𝑆 ∈ ℝ+ )
5 equivbnd2.5 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝑁 𝑦 ) ≤ ( 𝑅 · ( 𝑥 𝑀 𝑦 ) ) )
6 equivbnd2.6 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝑀 𝑦 ) ≤ ( 𝑆 · ( 𝑥 𝑁 𝑦 ) ) )
7 equivbnd2.7 ⊢ 𝐶 = ( 𝑀 ↾ ( 𝑌 × 𝑌 ) )
8 equivbnd2.8 ⊢ 𝐷 = ( 𝑁 ↾ ( 𝑌 × 𝑌 ) )
9 equivbnd2.9 ⊢ ( 𝜑 → ( 𝐶 ∈ ( TotBnd ‘ 𝑌 ) ↔ 𝐶 ∈ ( Bnd ‘ 𝑌 ) ) )
10 totbndbnd ⊢ ( 𝐷 ∈ ( TotBnd ‘ 𝑌 ) → 𝐷 ∈ ( Bnd ‘ 𝑌 ) )
11 simpr ⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( Bnd ‘ 𝑌 ) ) → 𝐷 ∈ ( Bnd ‘ 𝑌 ) )
12 1 adantr ⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( Bnd ‘ 𝑌 ) ) → 𝑀 ∈ ( Met ‘ 𝑋 ) )
13 8 bnd2lem ⊢ ( ( 𝑁 ∈ ( Met ‘ 𝑋 ) ∧ 𝐷 ∈ ( Bnd ‘ 𝑌 ) ) → 𝑌 ⊆ 𝑋 )
14 2 13 sylan ⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( Bnd ‘ 𝑌 ) ) → 𝑌 ⊆ 𝑋 )
15 metres2 ⊢ ( ( 𝑀 ∈ ( Met ‘ 𝑋 ) ∧ 𝑌 ⊆ 𝑋 ) → ( 𝑀 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( Met ‘ 𝑌 ) )
16 12 14 15 syl2anc ⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( Bnd ‘ 𝑌 ) ) → ( 𝑀 ↾ ( 𝑌 × 𝑌 ) ) ∈ ( Met ‘ 𝑌 ) )
17 7 16 eqeltrid ⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( Bnd ‘ 𝑌 ) ) → 𝐶 ∈ ( Met ‘ 𝑌 ) )
18 4 adantr ⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( Bnd ‘ 𝑌 ) ) → 𝑆 ∈ ℝ+ )
19 14 sselda ⊢ ( ( ( 𝜑 ∧ 𝐷 ∈ ( Bnd ‘ 𝑌 ) ) ∧ 𝑥 ∈ 𝑌 ) → 𝑥 ∈ 𝑋 )
20 14 sselda ⊢ ( ( ( 𝜑 ∧ 𝐷 ∈ ( Bnd ‘ 𝑌 ) ) ∧ 𝑦 ∈ 𝑌 ) → 𝑦 ∈ 𝑋 )
21 19 20 anim12dan ⊢ ( ( ( 𝜑 ∧ 𝐷 ∈ ( Bnd ‘ 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) )
22 6 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐷 ∈ ( Bnd ‘ 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝑀 𝑦 ) ≤ ( 𝑆 · ( 𝑥 𝑁 𝑦 ) ) )
23 21 22 syldan ⊢ ( ( ( 𝜑 ∧ 𝐷 ∈ ( Bnd ‘ 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝑥 𝑀 𝑦 ) ≤ ( 𝑆 · ( 𝑥 𝑁 𝑦 ) ) )
24 7 oveqi ⊢ ( 𝑥 𝐶 𝑦 ) = ( 𝑥 ( 𝑀 ↾ ( 𝑌 × 𝑌 ) ) 𝑦 )
25 ovres ⊢ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) → ( 𝑥 ( 𝑀 ↾ ( 𝑌 × 𝑌 ) ) 𝑦 ) = ( 𝑥 𝑀 𝑦 ) )
26 24 25 syl5eq ⊢ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) → ( 𝑥 𝐶 𝑦 ) = ( 𝑥 𝑀 𝑦 ) )
27 26 adantl ⊢ ( ( ( 𝜑 ∧ 𝐷 ∈ ( Bnd ‘ 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝑥 𝐶 𝑦 ) = ( 𝑥 𝑀 𝑦 ) )
28 8 oveqi ⊢ ( 𝑥 𝐷 𝑦 ) = ( 𝑥 ( 𝑁 ↾ ( 𝑌 × 𝑌 ) ) 𝑦 )
29 ovres ⊢ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) → ( 𝑥 ( 𝑁 ↾ ( 𝑌 × 𝑌 ) ) 𝑦 ) = ( 𝑥 𝑁 𝑦 ) )
30 28 29 syl5eq ⊢ ( ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) → ( 𝑥 𝐷 𝑦 ) = ( 𝑥 𝑁 𝑦 ) )
31 30 adantl ⊢ ( ( ( 𝜑 ∧ 𝐷 ∈ ( Bnd ‘ 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝑥 𝐷 𝑦 ) = ( 𝑥 𝑁 𝑦 ) )
32 31 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝐷 ∈ ( Bnd ‘ 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝑆 · ( 𝑥 𝐷 𝑦 ) ) = ( 𝑆 · ( 𝑥 𝑁 𝑦 ) ) )
33 23 27 32 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝐷 ∈ ( Bnd ‘ 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝑥 𝐶 𝑦 ) ≤ ( 𝑆 · ( 𝑥 𝐷 𝑦 ) ) )
34 11 17 18 33 equivbnd ⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( Bnd ‘ 𝑌 ) ) → 𝐶 ∈ ( Bnd ‘ 𝑌 ) )
35 9 biimpar ⊢ ( ( 𝜑 ∧ 𝐶 ∈ ( Bnd ‘ 𝑌 ) ) → 𝐶 ∈ ( TotBnd ‘ 𝑌 ) )
36 34 35 syldan ⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( Bnd ‘ 𝑌 ) ) → 𝐶 ∈ ( TotBnd ‘ 𝑌 ) )
37 bndmet ⊢ ( 𝐷 ∈ ( Bnd ‘ 𝑌 ) → 𝐷 ∈ ( Met ‘ 𝑌 ) )
38 37 adantl ⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( Bnd ‘ 𝑌 ) ) → 𝐷 ∈ ( Met ‘ 𝑌 ) )
39 3 adantr ⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( Bnd ‘ 𝑌 ) ) → 𝑅 ∈ ℝ+ )
40 5 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐷 ∈ ( Bnd ‘ 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 𝑁 𝑦 ) ≤ ( 𝑅 · ( 𝑥 𝑀 𝑦 ) ) )
41 21 40 syldan ⊢ ( ( ( 𝜑 ∧ 𝐷 ∈ ( Bnd ‘ 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝑥 𝑁 𝑦 ) ≤ ( 𝑅 · ( 𝑥 𝑀 𝑦 ) ) )
42 27 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝐷 ∈ ( Bnd ‘ 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝑅 · ( 𝑥 𝐶 𝑦 ) ) = ( 𝑅 · ( 𝑥 𝑀 𝑦 ) ) )
43 41 31 42 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝐷 ∈ ( Bnd ‘ 𝑌 ) ) ∧ ( 𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌 ) ) → ( 𝑥 𝐷 𝑦 ) ≤ ( 𝑅 · ( 𝑥 𝐶 𝑦 ) ) )
44 36 38 39 43 equivtotbnd ⊢ ( ( 𝜑 ∧ 𝐷 ∈ ( Bnd ‘ 𝑌 ) ) → 𝐷 ∈ ( TotBnd ‘ 𝑌 ) )
45 44 ex ⊢ ( 𝜑 → ( 𝐷 ∈ ( Bnd ‘ 𝑌 ) → 𝐷 ∈ ( TotBnd ‘ 𝑌 ) ) )
46 10 45 impbid2 ⊢ ( 𝜑 → ( 𝐷 ∈ ( TotBnd ‘ 𝑌 ) ↔ 𝐷 ∈ ( Bnd ‘ 𝑌 ) ) )