Metamath Proof Explorer

Theorem rrntotbnd

Description: A set in Euclidean space is totally bounded iff its is bounded. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 16-Sep-2015)

Ref Expression
Hypotheses rrntotbnd.1 ⊢ 𝑋 = ( ℝ ↑m 𝐼 )
rrntotbnd.2 ⊢ 𝑀 = ( ( ℝn ‘ 𝐼 ) ↾ ( 𝑌 × 𝑌 ) )
Assertion rrntotbnd ( 𝐼 ∈ Fin → ( 𝑀 ∈ ( TotBnd ‘ 𝑌 ) ↔ 𝑀 ∈ ( Bnd ‘ 𝑌 ) ) )

Proof

Step Hyp Ref Expression
1 rrntotbnd.1 ⊢ 𝑋 = ( ℝ ↑m 𝐼 )
2 rrntotbnd.2 ⊢ 𝑀 = ( ( ℝn ‘ 𝐼 ) ↾ ( 𝑌 × 𝑌 ) )
3 eqid ⊢ ( ( ℂfld ↾s ℝ ) ↑s 𝐼 ) = ( ( ℂfld ↾s ℝ ) ↑s 𝐼 )
4 eqid ⊢ ( dist ‘ ( ( ℂfld ↾s ℝ ) ↑s 𝐼 ) ) = ( dist ‘ ( ( ℂfld ↾s ℝ ) ↑s 𝐼 ) )
5 3 4 1 repwsmet ⊢ ( 𝐼 ∈ Fin → ( dist ‘ ( ( ℂfld ↾s ℝ ) ↑s 𝐼 ) ) ∈ ( Met ‘ 𝑋 ) )
6 1 rrnmet ⊢ ( 𝐼 ∈ Fin → ( ℝn ‘ 𝐼 ) ∈ ( Met ‘ 𝑋 ) )
7 hashcl ⊢ ( 𝐼 ∈ Fin → ( ♯ ‘ 𝐼 ) ∈ ℕ0 )
8 nn0re ⊢ ( ( ♯ ‘ 𝐼 ) ∈ ℕ0 → ( ♯ ‘ 𝐼 ) ∈ ℝ )
9 nn0ge0 ⊢ ( ( ♯ ‘ 𝐼 ) ∈ ℕ0 → 0 ≤ ( ♯ ‘ 𝐼 ) )
10 8 9 resqrtcld ⊢ ( ( ♯ ‘ 𝐼 ) ∈ ℕ0 → ( √ ‘ ( ♯ ‘ 𝐼 ) ) ∈ ℝ )
11 7 10 syl ⊢ ( 𝐼 ∈ Fin → ( √ ‘ ( ♯ ‘ 𝐼 ) ) ∈ ℝ )
12 8 9 sqrtge0d ⊢ ( ( ♯ ‘ 𝐼 ) ∈ ℕ0 → 0 ≤ ( √ ‘ ( ♯ ‘ 𝐼 ) ) )
13 7 12 syl ⊢ ( 𝐼 ∈ Fin → 0 ≤ ( √ ‘ ( ♯ ‘ 𝐼 ) ) )
14 11 13 ge0p1rpd ⊢ ( 𝐼 ∈ Fin → ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) + 1 ) ∈ ℝ+ )
15 1rp ⊢ 1 ∈ ℝ+
16 15 a1i ⊢ ( 𝐼 ∈ Fin → 1 ∈ ℝ+ )
17 metcl ⊢ ( ( ( ℝn ‘ 𝐼 ) ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 ( ℝn ‘ 𝐼 ) 𝑦 ) ∈ ℝ )
18 17 3expb ⊢ ( ( ( ℝn ‘ 𝐼 ) ∈ ( Met ‘ 𝑋 ) ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ( ℝn ‘ 𝐼 ) 𝑦 ) ∈ ℝ )
19 6 18 sylan ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ( ℝn ‘ 𝐼 ) 𝑦 ) ∈ ℝ )
20 11 adantr ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( √ ‘ ( ♯ ‘ 𝐼 ) ) ∈ ℝ )
21 5 adantr ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( dist ‘ ( ( ℂfld ↾s ℝ ) ↑s 𝐼 ) ) ∈ ( Met ‘ 𝑋 ) )
22 simprl ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑥 ∈ 𝑋 )
23 simprr ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → 𝑦 ∈ 𝑋 )
24 metcl ⊢ ( ( ( dist ‘ ( ( ℂfld ↾s ℝ ) ↑s 𝐼 ) ) ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝑥 ( dist ‘ ( ( ℂfld ↾s ℝ ) ↑s 𝐼 ) ) 𝑦 ) ∈ ℝ )
25 metge0 ⊢ ( ( ( dist ‘ ( ( ℂfld ↾s ℝ ) ↑s 𝐼 ) ) ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → 0 ≤ ( 𝑥 ( dist ‘ ( ( ℂfld ↾s ℝ ) ↑s 𝐼 ) ) 𝑦 ) )
26 24 25 jca ⊢ ( ( ( dist ‘ ( ( ℂfld ↾s ℝ ) ↑s 𝐼 ) ) ∈ ( Met ‘ 𝑋 ) ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( ( 𝑥 ( dist ‘ ( ( ℂfld ↾s ℝ ) ↑s 𝐼 ) ) 𝑦 ) ∈ ℝ ∧ 0 ≤ ( 𝑥 ( dist ‘ ( ( ℂfld ↾s ℝ ) ↑s 𝐼 ) ) 𝑦 ) ) )
27 21 22 23 26 syl3anc ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 ( dist ‘ ( ( ℂfld ↾s ℝ ) ↑s 𝐼 ) ) 𝑦 ) ∈ ℝ ∧ 0 ≤ ( 𝑥 ( dist ‘ ( ( ℂfld ↾s ℝ ) ↑s 𝐼 ) ) 𝑦 ) ) )
28 27 simpld ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ( dist ‘ ( ( ℂfld ↾s ℝ ) ↑s 𝐼 ) ) 𝑦 ) ∈ ℝ )
29 20 28 remulcld ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) · ( 𝑥 ( dist ‘ ( ( ℂfld ↾s ℝ ) ↑s 𝐼 ) ) 𝑦 ) ) ∈ ℝ )
30 peano2re ⊢ ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) ∈ ℝ → ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) + 1 ) ∈ ℝ )
31 11 30 syl ⊢ ( 𝐼 ∈ Fin → ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) + 1 ) ∈ ℝ )
32 31 adantr ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) + 1 ) ∈ ℝ )
33 32 28 remulcld ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) + 1 ) · ( 𝑥 ( dist ‘ ( ( ℂfld ↾s ℝ ) ↑s 𝐼 ) ) 𝑦 ) ) ∈ ℝ )
34 id ⊢ ( 𝐼 ∈ Fin → 𝐼 ∈ Fin )
35 3 4 1 34 rrnequiv ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( 𝑥 ( dist ‘ ( ( ℂfld ↾s ℝ ) ↑s 𝐼 ) ) 𝑦 ) ≤ ( 𝑥 ( ℝn ‘ 𝐼 ) 𝑦 ) ∧ ( 𝑥 ( ℝn ‘ 𝐼 ) 𝑦 ) ≤ ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) · ( 𝑥 ( dist ‘ ( ( ℂfld ↾s ℝ ) ↑s 𝐼 ) ) 𝑦 ) ) ) )
36 35 simprd ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ( ℝn ‘ 𝐼 ) 𝑦 ) ≤ ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) · ( 𝑥 ( dist ‘ ( ( ℂfld ↾s ℝ ) ↑s 𝐼 ) ) 𝑦 ) ) )
37 20 lep1d ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( √ ‘ ( ♯ ‘ 𝐼 ) ) ≤ ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) + 1 ) )
38 lemul1a ⊢ ( ( ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) ∈ ℝ ∧ ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) + 1 ) ∈ ℝ ∧ ( ( 𝑥 ( dist ‘ ( ( ℂfld ↾s ℝ ) ↑s 𝐼 ) ) 𝑦 ) ∈ ℝ ∧ 0 ≤ ( 𝑥 ( dist ‘ ( ( ℂfld ↾s ℝ ) ↑s 𝐼 ) ) 𝑦 ) ) ) ∧ ( √ ‘ ( ♯ ‘ 𝐼 ) ) ≤ ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) + 1 ) ) → ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) · ( 𝑥 ( dist ‘ ( ( ℂfld ↾s ℝ ) ↑s 𝐼 ) ) 𝑦 ) ) ≤ ( ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) + 1 ) · ( 𝑥 ( dist ‘ ( ( ℂfld ↾s ℝ ) ↑s 𝐼 ) ) 𝑦 ) ) )
39 20 32 27 37 38 syl31anc ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) · ( 𝑥 ( dist ‘ ( ( ℂfld ↾s ℝ ) ↑s 𝐼 ) ) 𝑦 ) ) ≤ ( ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) + 1 ) · ( 𝑥 ( dist ‘ ( ( ℂfld ↾s ℝ ) ↑s 𝐼 ) ) 𝑦 ) ) )
40 19 29 33 36 39 letrd ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ( ℝn ‘ 𝐼 ) 𝑦 ) ≤ ( ( ( √ ‘ ( ♯ ‘ 𝐼 ) ) + 1 ) · ( 𝑥 ( dist ‘ ( ( ℂfld ↾s ℝ ) ↑s 𝐼 ) ) 𝑦 ) ) )
41 35 simpld ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ( dist ‘ ( ( ℂfld ↾s ℝ ) ↑s 𝐼 ) ) 𝑦 ) ≤ ( 𝑥 ( ℝn ‘ 𝐼 ) 𝑦 ) )
42 19 recnd ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ( ℝn ‘ 𝐼 ) 𝑦 ) ∈ ℂ )
43 42 mullidd ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 1 · ( 𝑥 ( ℝn ‘ 𝐼 ) 𝑦 ) ) = ( 𝑥 ( ℝn ‘ 𝐼 ) 𝑦 ) )
44 41 43 breqtrrd ⊢ ( ( 𝐼 ∈ Fin ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝑥 ( dist ‘ ( ( ℂfld ↾s ℝ ) ↑s 𝐼 ) ) 𝑦 ) ≤ ( 1 · ( 𝑥 ( ℝn ‘ 𝐼 ) 𝑦 ) ) )
45 eqid ⊢ ( ( dist ‘ ( ( ℂfld ↾s ℝ ) ↑s 𝐼 ) ) ↾ ( 𝑌 × 𝑌 ) ) = ( ( dist ‘ ( ( ℂfld ↾s ℝ ) ↑s 𝐼 ) ) ↾ ( 𝑌 × 𝑌 ) )
46 ax-resscn ⊢ ℝ ⊆ ℂ
47 3 45 cnpwstotbnd ⊢ ( ( ℝ ⊆ ℂ ∧ 𝐼 ∈ Fin ) → ( ( ( dist ‘ ( ( ℂfld ↾s ℝ ) ↑s 𝐼 ) ) ↾ ( 𝑌 × 𝑌 ) ) ∈ ( TotBnd ‘ 𝑌 ) ↔ ( ( dist ‘ ( ( ℂfld ↾s ℝ ) ↑s 𝐼 ) ) ↾ ( 𝑌 × 𝑌 ) ) ∈ ( Bnd ‘ 𝑌 ) ) )
48 46 47 mpan ⊢ ( 𝐼 ∈ Fin → ( ( ( dist ‘ ( ( ℂfld ↾s ℝ ) ↑s 𝐼 ) ) ↾ ( 𝑌 × 𝑌 ) ) ∈ ( TotBnd ‘ 𝑌 ) ↔ ( ( dist ‘ ( ( ℂfld ↾s ℝ ) ↑s 𝐼 ) ) ↾ ( 𝑌 × 𝑌 ) ) ∈ ( Bnd ‘ 𝑌 ) ) )
49 5 6 14 16 40 44 45 2 48 equivbnd2 ⊢ ( 𝐼 ∈ Fin → ( 𝑀 ∈ ( TotBnd ‘ 𝑌 ) ↔ 𝑀 ∈ ( Bnd ‘ 𝑌 ) ) )