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	$⊢ X = ℝ^{I}$
	rrntotbnd.2	$⊢ M = {ℝ^{n} (I) ↾}_{(Y \times Y)}$
Assertion	rrntotbnd	$⊢ I \in Fin \to (M \in TotBnd (Y) \leftrightarrow M \in Bnd (Y))$

Proof

Step	Hyp	Ref	Expression
1		rrntotbnd.1	$⊢ X = ℝ^{I}$
2		rrntotbnd.2	$⊢ M = {ℝ^{n} (I) ↾}_{(Y \times Y)}$
3		eqid	$⊢ (ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I = (ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I$
4		eqid	$⊢ dist ((ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I) = dist ((ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I)$
5	3 4 1	repwsmet	$⊢ I \in Fin \to dist ((ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I) \in Met (X)$
6	1	rrnmet	$⊢ I \in Fin \to ℝ^{n} (I) \in Met (X)$
7		hashcl	$⊢ I \in Fin \to \|I\| \in ℕ_{0}$
8		nn0re	$⊢ \|I\| \in ℕ_{0} \to \|I\| \in ℝ$
9		nn0ge0	$⊢ \|I\| \in ℕ_{0} \to 0 \leq \|I\|$
10	8 9	resqrtcld	$⊢ \|I\| \in ℕ_{0} \to \sqrt{\|I\|} \in ℝ$
11	7 10	syl	$⊢ I \in Fin \to \sqrt{\|I\|} \in ℝ$
12	8 9	sqrtge0d	$⊢ \|I\| \in ℕ_{0} \to 0 \leq \sqrt{\|I\|}$
13	7 12	syl	$⊢ I \in Fin \to 0 \leq \sqrt{\|I\|}$
14	11 13	ge0p1rpd	$⊢ I \in Fin \to \sqrt{\|I\|} + 1 \in ℝ^{+}$
15		1rp	$⊢ 1 \in ℝ^{+}$
16	15	a1i	$⊢ I \in Fin \to 1 \in ℝ^{+}$
17		metcl	$⊢ (ℝ^{n} (I) \in Met (X) \land x \in X \land y \in X) \to x ℝ^{n} (I) y \in ℝ$
18	17	3expb	$⊢ (ℝ^{n} (I) \in Met (X) \land (x \in X \land y \in X)) \to x ℝ^{n} (I) y \in ℝ$
19	6 18	sylan	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to x ℝ^{n} (I) y \in ℝ$
20	11	adantr	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to \sqrt{\|I\|} \in ℝ$
21	5	adantr	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to dist ((ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I) \in Met (X)$
22		simprl	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to x \in X$
23		simprr	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to y \in X$
24		metcl	$⊢ (dist ((ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I) \in Met (X) \land x \in X \land y \in X) \to x dist ((ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I) y \in ℝ$
25		metge0	$⊢ (dist ((ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I) \in Met (X) \land x \in X \land y \in X) \to 0 \leq x dist ((ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I) y$
26	24 25	jca	$⊢ (dist ((ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I) \in Met (X) \land x \in X \land y \in X) \to (x dist ((ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I) y \in ℝ \land 0 \leq x dist ((ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I) y)$
27	21 22 23 26	syl3anc	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to (x dist ((ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I) y \in ℝ \land 0 \leq x dist ((ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I) y)$
28	27	simpld	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to x dist ((ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I) y \in ℝ$
29	20 28	remulcld	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to \sqrt{\|I\|} (x dist ((ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I) y) \in ℝ$
30		peano2re	$⊢ \sqrt{\|I\|} \in ℝ \to \sqrt{\|I\|} + 1 \in ℝ$
31	11 30	syl	$⊢ I \in Fin \to \sqrt{\|I\|} + 1 \in ℝ$
32	31	adantr	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to \sqrt{\|I\|} + 1 \in ℝ$
33	32 28	remulcld	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to (\sqrt{\|I\|} + 1) (x dist ((ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I) y) \in ℝ$
34		id	$⊢ I \in Fin \to I \in Fin$
35	3 4 1 34	rrnequiv	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to (x dist ((ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I) y \leq x ℝ^{n} (I) y \land x ℝ^{n} (I) y \leq \sqrt{\|I\|} (x dist ((ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I) y))$
36	35	simprd	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to x ℝ^{n} (I) y \leq \sqrt{\|I\|} (x dist ((ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I) y)$
37	20	lep1d	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to \sqrt{\|I\|} \leq \sqrt{\|I\|} + 1$
38		lemul1a	$⊢ ((\sqrt{\|I\|} \in ℝ \land \sqrt{\|I\|} + 1 \in ℝ \land (x dist ((ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I) y \in ℝ \land 0 \leq x dist ((ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I) y)) \land \sqrt{\|I\|} \leq \sqrt{\|I\|} + 1) \to \sqrt{\|I\|} (x dist ((ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I) y) \leq (\sqrt{\|I\|} + 1) (x dist ((ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I) y)$
39	20 32 27 37 38	syl31anc	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to \sqrt{\|I\|} (x dist ((ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I) y) \leq (\sqrt{\|I\|} + 1) (x dist ((ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I) y)$
40	19 29 33 36 39	letrd	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to x ℝ^{n} (I) y \leq (\sqrt{\|I\|} + 1) (x dist ((ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I) y)$
41	35	simpld	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to x dist ((ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I) y \leq x ℝ^{n} (I) y$
42	19	recnd	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to x ℝ^{n} (I) y \in ℂ$
43	42	mulid2d	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to 1 (x ℝ^{n} (I) y) = x ℝ^{n} (I) y$
44	41 43	breqtrrd	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to x dist ((ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I) y \leq 1 (x ℝ^{n} (I) y)$
45		eqid	$⊢ {dist ((ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I) ↾}_{(Y \times Y)} = {dist ((ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I) ↾}_{(Y \times Y)}$
46		ax-resscn	$⊢ ℝ \subseteq ℂ$
47	3 45	cnpwstotbnd	$⊢ (ℝ \subseteq ℂ \land I \in Fin) \to ({dist ((ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I) ↾}_{(Y \times Y)} \in TotBnd (Y) \leftrightarrow {dist ((ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I) ↾}_{(Y \times Y)} \in Bnd (Y))$
48	46 47	mpan	$⊢ I \in Fin \to ({dist ((ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I) ↾}_{(Y \times Y)} \in TotBnd (Y) \leftrightarrow {dist ((ℂ_{fld} ↾_{𝑠} ℝ) ↑_{𝑠} I) ↾}_{(Y \times Y)} \in Bnd (Y))$
49	5 6 14 16 40 44 45 2 48	equivbnd2	$⊢ I \in Fin \to (M \in TotBnd (Y) \leftrightarrow M \in Bnd (Y))$

Metamath Proof Explorer

Theorem rrntotbnd

Proof