rrnmet

Description: Euclidean space is a metric space. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 5-Jun-2014)

		Ref	Expression
	Hypothesis	rrnval.1	$⊢ X = ℝ^{I}$
	Assertion	rrnmet	$⊢ I \in Fin \to ℝ^{n} (I) \in Met (X)$

Proof

Step	Hyp	Ref	Expression
1		rrnval.1	$⊢ X = ℝ^{I}$
2		simpl	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to I \in Fin$
3		simprl	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to x \in X$
4	3 1	eleqtrdi	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to x \in (ℝ^{I})$
5		elmapi	$⊢ x \in (ℝ^{I}) \to x : I ⟶ ℝ$
6	4 5	syl	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to x : I ⟶ ℝ$
7	6	ffvelrnda	$⊢ ((I \in Fin \land (x \in X \land y \in X)) \land k \in I) \to x (k) \in ℝ$
8		simprr	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to y \in X$
9	8 1	eleqtrdi	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to y \in (ℝ^{I})$
10		elmapi	$⊢ y \in (ℝ^{I}) \to y : I ⟶ ℝ$
11	9 10	syl	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to y : I ⟶ ℝ$
12	11	ffvelrnda	$⊢ ((I \in Fin \land (x \in X \land y \in X)) \land k \in I) \to y (k) \in ℝ$
13	7 12	resubcld	$⊢ ((I \in Fin \land (x \in X \land y \in X)) \land k \in I) \to x (k) - y (k) \in ℝ$
14	13	resqcld	$⊢ ((I \in Fin \land (x \in X \land y \in X)) \land k \in I) \to {(x (k) - y (k))}^{2} \in ℝ$
15	2 14	fsumrecl	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to \sum_{k \in I} {(x (k) - y (k))}^{2} \in ℝ$
16	13	sqge0d	$⊢ ((I \in Fin \land (x \in X \land y \in X)) \land k \in I) \to 0 \leq {(x (k) - y (k))}^{2}$
17	2 14 16	fsumge0	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to 0 \leq \sum_{k \in I} {(x (k) - y (k))}^{2}$
18	15 17	resqrtcld	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to \sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}} \in ℝ$
19	18	ralrimivva	$⊢ I \in Fin \to \forall x \in X \forall y \in X \sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}} \in ℝ$
20		eqid	$⊢ (x \in X, y \in X ⟼ \sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}}) = (x \in X, y \in X ⟼ \sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}})$
21	20	fmpo	$⊢ \forall x \in X \forall y \in X \sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}} \in ℝ \leftrightarrow (x \in X, y \in X ⟼ \sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}}) : X \times X ⟶ ℝ$
22	19 21	sylib	$⊢ I \in Fin \to (x \in X, y \in X ⟼ \sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}}) : X \times X ⟶ ℝ$
23	1	rrnval	$⊢ I \in Fin \to ℝ^{n} (I) = (x \in X, y \in X ⟼ \sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}})$
24	23	feq1d	$⊢ I \in Fin \to (ℝ^{n} (I) : X \times X ⟶ ℝ \leftrightarrow (x \in X, y \in X ⟼ \sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}}) : X \times X ⟶ ℝ)$
25	22 24	mpbird	$⊢ I \in Fin \to ℝ^{n} (I) : X \times X ⟶ ℝ$
26		sqrt00	$⊢ (\sum_{k \in I} {(x (k) - y (k))}^{2} \in ℝ \land 0 \leq \sum_{k \in I} {(x (k) - y (k))}^{2}) \to (\sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}} = 0 \leftrightarrow \sum_{k \in I} {(x (k) - y (k))}^{2} = 0)$
27	15 17 26	syl2anc	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to (\sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}} = 0 \leftrightarrow \sum_{k \in I} {(x (k) - y (k))}^{2} = 0)$
28	2 14 16	fsum00	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to (\sum_{k \in I} {(x (k) - y (k))}^{2} = 0 \leftrightarrow \forall k \in I {(x (k) - y (k))}^{2} = 0)$
29	27 28	bitrd	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to (\sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}} = 0 \leftrightarrow \forall k \in I {(x (k) - y (k))}^{2} = 0)$
30	13	recnd	$⊢ ((I \in Fin \land (x \in X \land y \in X)) \land k \in I) \to x (k) - y (k) \in ℂ$
31		sqeq0	$⊢ x (k) - y (k) \in ℂ \to ({(x (k) - y (k))}^{2} = 0 \leftrightarrow x (k) - y (k) = 0)$
32	30 31	syl	$⊢ ((I \in Fin \land (x \in X \land y \in X)) \land k \in I) \to ({(x (k) - y (k))}^{2} = 0 \leftrightarrow x (k) - y (k) = 0)$
33	7	recnd	$⊢ ((I \in Fin \land (x \in X \land y \in X)) \land k \in I) \to x (k) \in ℂ$
34	12	recnd	$⊢ ((I \in Fin \land (x \in X \land y \in X)) \land k \in I) \to y (k) \in ℂ$
35	33 34	subeq0ad	$⊢ ((I \in Fin \land (x \in X \land y \in X)) \land k \in I) \to (x (k) - y (k) = 0 \leftrightarrow x (k) = y (k))$
36	32 35	bitrd	$⊢ ((I \in Fin \land (x \in X \land y \in X)) \land k \in I) \to ({(x (k) - y (k))}^{2} = 0 \leftrightarrow x (k) = y (k))$
37	36	ralbidva	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to (\forall k \in I {(x (k) - y (k))}^{2} = 0 \leftrightarrow \forall k \in I x (k) = y (k))$
38	29 37	bitrd	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to (\sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}} = 0 \leftrightarrow \forall k \in I x (k) = y (k))$
39	1	rrnmval	$⊢ (I \in Fin \land x \in X \land y \in X) \to x ℝ^{n} (I) y = \sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}}$
40	39	3expb	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to x ℝ^{n} (I) y = \sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}}$
41	40	eqeq1d	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to (x ℝ^{n} (I) y = 0 \leftrightarrow \sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}} = 0)$
42	6	ffnd	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to x Fn I$
43	11	ffnd	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to y Fn I$
44		eqfnfv	$⊢ (x Fn I \land y Fn I) \to (x = y \leftrightarrow \forall k \in I x (k) = y (k))$
45	42 43 44	syl2anc	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to (x = y \leftrightarrow \forall k \in I x (k) = y (k))$
46	38 41 45	3bitr4d	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to (x ℝ^{n} (I) y = 0 \leftrightarrow x = y)$
47		simpll	$⊢ ((I \in Fin \land (x \in X \land y \in X)) \land z \in X) \to I \in Fin$
48	7	adantlr	$⊢ (((I \in Fin \land (x \in X \land y \in X)) \land z \in X) \land k \in I) \to x (k) \in ℝ$
49		simpr	$⊢ ((I \in Fin \land (x \in X \land y \in X)) \land z \in X) \to z \in X$
50	49 1	eleqtrdi	$⊢ ((I \in Fin \land (x \in X \land y \in X)) \land z \in X) \to z \in (ℝ^{I})$
51		elmapi	$⊢ z \in (ℝ^{I}) \to z : I ⟶ ℝ$
52	50 51	syl	$⊢ ((I \in Fin \land (x \in X \land y \in X)) \land z \in X) \to z : I ⟶ ℝ$
53	52	ffvelrnda	$⊢ (((I \in Fin \land (x \in X \land y \in X)) \land z \in X) \land k \in I) \to z (k) \in ℝ$
54	48 53	resubcld	$⊢ (((I \in Fin \land (x \in X \land y \in X)) \land z \in X) \land k \in I) \to x (k) - z (k) \in ℝ$
55	12	adantlr	$⊢ (((I \in Fin \land (x \in X \land y \in X)) \land z \in X) \land k \in I) \to y (k) \in ℝ$
56	53 55	resubcld	$⊢ (((I \in Fin \land (x \in X \land y \in X)) \land z \in X) \land k \in I) \to z (k) - y (k) \in ℝ$
57	47 54 56	trirn	$⊢ ((I \in Fin \land (x \in X \land y \in X)) \land z \in X) \to \sqrt{\sum_{k \in I} {((x (k) - z (k)) + z (k) - y (k))}^{2}} \leq \sqrt{\sum_{k \in I} {(x (k) - z (k))}^{2}} + \sqrt{\sum_{k \in I} {(z (k) - y (k))}^{2}}$
58	33	adantlr	$⊢ (((I \in Fin \land (x \in X \land y \in X)) \land z \in X) \land k \in I) \to x (k) \in ℂ$
59	53	recnd	$⊢ (((I \in Fin \land (x \in X \land y \in X)) \land z \in X) \land k \in I) \to z (k) \in ℂ$
60	34	adantlr	$⊢ (((I \in Fin \land (x \in X \land y \in X)) \land z \in X) \land k \in I) \to y (k) \in ℂ$
61	58 59 60	npncand	$⊢ (((I \in Fin \land (x \in X \land y \in X)) \land z \in X) \land k \in I) \to (x (k) - z (k)) + z (k) - y (k) = x (k) - y (k)$
62	61	oveq1d	$⊢ (((I \in Fin \land (x \in X \land y \in X)) \land z \in X) \land k \in I) \to {((x (k) - z (k)) + z (k) - y (k))}^{2} = {(x (k) - y (k))}^{2}$
63	62	sumeq2dv	$⊢ ((I \in Fin \land (x \in X \land y \in X)) \land z \in X) \to \sum_{k \in I} {((x (k) - z (k)) + z (k) - y (k))}^{2} = \sum_{k \in I} {(x (k) - y (k))}^{2}$
64	63	fveq2d	$⊢ ((I \in Fin \land (x \in X \land y \in X)) \land z \in X) \to \sqrt{\sum_{k \in I} {((x (k) - z (k)) + z (k) - y (k))}^{2}} = \sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}}$
65		sqsubswap	$⊢ (x (k) \in ℂ \land z (k) \in ℂ) \to {(x (k) - z (k))}^{2} = {(z (k) - x (k))}^{2}$
66	58 59 65	syl2anc	$⊢ (((I \in Fin \land (x \in X \land y \in X)) \land z \in X) \land k \in I) \to {(x (k) - z (k))}^{2} = {(z (k) - x (k))}^{2}$
67	66	sumeq2dv	$⊢ ((I \in Fin \land (x \in X \land y \in X)) \land z \in X) \to \sum_{k \in I} {(x (k) - z (k))}^{2} = \sum_{k \in I} {(z (k) - x (k))}^{2}$
68	67	fveq2d	$⊢ ((I \in Fin \land (x \in X \land y \in X)) \land z \in X) \to \sqrt{\sum_{k \in I} {(x (k) - z (k))}^{2}} = \sqrt{\sum_{k \in I} {(z (k) - x (k))}^{2}}$
69	68	oveq1d	$⊢ ((I \in Fin \land (x \in X \land y \in X)) \land z \in X) \to \sqrt{\sum_{k \in I} {(x (k) - z (k))}^{2}} + \sqrt{\sum_{k \in I} {(z (k) - y (k))}^{2}} = \sqrt{\sum_{k \in I} {(z (k) - x (k))}^{2}} + \sqrt{\sum_{k \in I} {(z (k) - y (k))}^{2}}$
70	57 64 69	3brtr3d	$⊢ ((I \in Fin \land (x \in X \land y \in X)) \land z \in X) \to \sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}} \leq \sqrt{\sum_{k \in I} {(z (k) - x (k))}^{2}} + \sqrt{\sum_{k \in I} {(z (k) - y (k))}^{2}}$
71	40	adantr	$⊢ ((I \in Fin \land (x \in X \land y \in X)) \land z \in X) \to x ℝ^{n} (I) y = \sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}}$
72	1	rrnmval	$⊢ (I \in Fin \land z \in X \land x \in X) \to z ℝ^{n} (I) x = \sqrt{\sum_{k \in I} {(z (k) - x (k))}^{2}}$
73	72	3adant3r	$⊢ (I \in Fin \land z \in X \land (x \in X \land y \in X)) \to z ℝ^{n} (I) x = \sqrt{\sum_{k \in I} {(z (k) - x (k))}^{2}}$
74	1	rrnmval	$⊢ (I \in Fin \land z \in X \land y \in X) \to z ℝ^{n} (I) y = \sqrt{\sum_{k \in I} {(z (k) - y (k))}^{2}}$
75	74	3adant3l	$⊢ (I \in Fin \land z \in X \land (x \in X \land y \in X)) \to z ℝ^{n} (I) y = \sqrt{\sum_{k \in I} {(z (k) - y (k))}^{2}}$
76	73 75	oveq12d	$⊢ (I \in Fin \land z \in X \land (x \in X \land y \in X)) \to (z ℝ^{n} (I) x) + (z ℝ^{n} (I) y) = \sqrt{\sum_{k \in I} {(z (k) - x (k))}^{2}} + \sqrt{\sum_{k \in I} {(z (k) - y (k))}^{2}}$
77	76	3expa	$⊢ ((I \in Fin \land z \in X) \land (x \in X \land y \in X)) \to (z ℝ^{n} (I) x) + (z ℝ^{n} (I) y) = \sqrt{\sum_{k \in I} {(z (k) - x (k))}^{2}} + \sqrt{\sum_{k \in I} {(z (k) - y (k))}^{2}}$
78	77	an32s	$⊢ ((I \in Fin \land (x \in X \land y \in X)) \land z \in X) \to (z ℝ^{n} (I) x) + (z ℝ^{n} (I) y) = \sqrt{\sum_{k \in I} {(z (k) - x (k))}^{2}} + \sqrt{\sum_{k \in I} {(z (k) - y (k))}^{2}}$
79	70 71 78	3brtr4d	$⊢ ((I \in Fin \land (x \in X \land y \in X)) \land z \in X) \to x ℝ^{n} (I) y \leq (z ℝ^{n} (I) x) + (z ℝ^{n} (I) y)$
80	79	ralrimiva	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to \forall z \in X x ℝ^{n} (I) y \leq (z ℝ^{n} (I) x) + (z ℝ^{n} (I) y)$
81	46 80	jca	$⊢ (I \in Fin \land (x \in X \land y \in X)) \to ((x ℝ^{n} (I) y = 0 \leftrightarrow x = y) \land \forall z \in X x ℝ^{n} (I) y \leq (z ℝ^{n} (I) x) + (z ℝ^{n} (I) y))$
82	81	ralrimivva	$⊢ I \in Fin \to \forall x \in X \forall y \in X ((x ℝ^{n} (I) y = 0 \leftrightarrow x = y) \land \forall z \in X x ℝ^{n} (I) y \leq (z ℝ^{n} (I) x) + (z ℝ^{n} (I) y))$
83		ovex	$⊢ ℝ^{I} \in V$
84	1 83	eqeltri	$⊢ X \in V$
85		ismet	$⊢ X \in V \to (ℝ^{n} (I) \in Met (X) \leftrightarrow (ℝ^{n} (I) : X \times X ⟶ ℝ \land \forall x \in X \forall y \in X ((x ℝ^{n} (I) y = 0 \leftrightarrow x = y) \land \forall z \in X x ℝ^{n} (I) y \leq (z ℝ^{n} (I) x) + (z ℝ^{n} (I) y))))$
86	84 85	ax-mp	$⊢ ℝ^{n} (I) \in Met (X) \leftrightarrow (ℝ^{n} (I) : X \times X ⟶ ℝ \land \forall x \in X \forall y \in X ((x ℝ^{n} (I) y = 0 \leftrightarrow x = y) \land \forall z \in X x ℝ^{n} (I) y \leq (z ℝ^{n} (I) x) + (z ℝ^{n} (I) y)))$
87	25 82 86	sylanbrc	$⊢ I \in Fin \to ℝ^{n} (I) \in Met (X)$

Metamath Proof Explorer

Theorem rrnmet

Proof