rrnval

Description: The n-dimensional Euclidean space. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 13-Sep-2015)

		Ref	Expression
	Hypothesis	rrnval.1	$⊢ X = ℝ^{I}$
	Assertion	rrnval	$⊢ I \in Fin \to ℝ^{n} (I) = (x \in X, y \in X ⟼ \sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}})$

Proof

Step	Hyp	Ref	Expression
1		rrnval.1	$⊢ X = ℝ^{I}$
2		oveq2	$⊢ i = I \to ℝ^{i} = ℝ^{I}$
3	2 1	eqtr4di	$⊢ i = I \to ℝ^{i} = X$
4		sumeq1	$⊢ i = I \to \sum_{k \in i} {(x (k) - y (k))}^{2} = \sum_{k \in I} {(x (k) - y (k))}^{2}$
5	4	fveq2d	$⊢ i = I \to \sqrt{\sum_{k \in i} {(x (k) - y (k))}^{2}} = \sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}}$
6	3 3 5	mpoeq123dv	$⊢ i = I \to (x \in (ℝ^{i}), y \in (ℝ^{i}) ⟼ \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}})$
7		df-rrn	$⊢ ℝ^{n} = (i \in Fin ⟼ (x \in (ℝ^{i}), y \in (ℝ^{i}) ⟼ \sqrt{\sum_{k \in i} {(x (k) - y (k))}^{2}}))$
8		fvrn0	$⊢ \sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}} \in (ran \sqrt \cup \{\emptyset\})$
9	8	rgen2w	$⊢ \forall x \in X \forall y \in X \sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}} \in (ran \sqrt \cup \{\emptyset\})$
10		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}})$
11	10	fmpo	$⊢ \forall x \in X \forall y \in X \sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}} \in (ran \sqrt \cup \{\emptyset\}) \leftrightarrow (x \in X, y \in X ⟼ \sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}}) : X \times X ⟶ ran \sqrt \cup \{\emptyset\}$
12	9 11	mpbi	$⊢ (x \in X, y \in X ⟼ \sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}}) : X \times X ⟶ ran \sqrt \cup \{\emptyset\}$
13		ovex	$⊢ ℝ^{I} \in V$
14	1 13	eqeltri	$⊢ X \in V$
15	14 14	xpex	$⊢ X \times X \in V$
16		cnex	$⊢ ℂ \in V$
17		sqrtf	$⊢ \sqrt : ℂ ⟶ ℂ$
18		frn	$⊢ \sqrt : ℂ ⟶ ℂ \to ran \sqrt \subseteq ℂ$
19	17 18	ax-mp	$⊢ ran \sqrt \subseteq ℂ$
20	16 19	ssexi	$⊢ ran \sqrt \in V$
21		p0ex	$⊢ \{\emptyset\} \in V$
22	20 21	unex	$⊢ ran \sqrt \cup \{\emptyset\} \in V$
23		fex2	$⊢ ((x \in X, y \in X ⟼ \sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}}) : X \times X ⟶ ran \sqrt \cup \{\emptyset\} \land X \times X \in V \land ran \sqrt \cup \{\emptyset\} \in V) \to (x \in X, y \in X ⟼ \sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}}) \in V$
24	12 15 22 23	mp3an	$⊢ (x \in X, y \in X ⟼ \sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}}) \in V$
25	6 7 24	fvmpt	$⊢ I \in Fin \to ℝ^{n} (I) = (x \in X, y \in X ⟼ \sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}})$

Metamath Proof Explorer

Theorem rrnval

Proof