rrnmval

Description: The value of the Euclidean metric. (Contributed by Jeff Madsen, 2-Sep-2009) (Revised by Mario Carneiro, 13-Sep-2015)

		Ref	Expression
	Hypothesis	rrnval.1	$⊢ X = ℝ^{I}$
	Assertion	rrnmval	$⊢ (I \in Fin \land F \in X \land G \in X) \to F ℝ^{n} (I) G = \sqrt{\sum_{k \in I} {(F (k) - G (k))}^{2}}$

Step	Hyp	Ref	Expression
1		rrnval.1	$⊢ X = ℝ^{I}$
2	1	rrnval	$⊢ I \in Fin \to ℝ^{n} (I) = (x \in X, y \in X ⟼ \sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}})$
3	2	3ad2ant1	$⊢ (I \in Fin \land F \in X \land G \in X) \to ℝ^{n} (I) = (x \in X, y \in X ⟼ \sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}})$
4		fveq1	$⊢ x = F \to x (k) = F (k)$
5		fveq1	$⊢ y = G \to y (k) = G (k)$
6	4 5	oveqan12d	$⊢ (x = F \land y = G) \to x (k) - y (k) = F (k) - G (k)$
7	6	oveq1d	$⊢ (x = F \land y = G) \to {(x (k) - y (k))}^{2} = {(F (k) - G (k))}^{2}$
8	7	sumeq2sdv	$⊢ (x = F \land y = G) \to \sum_{k \in I} {(x (k) - y (k))}^{2} = \sum_{k \in I} {(F (k) - G (k))}^{2}$
9	8	fveq2d	$⊢ (x = F \land y = G) \to \sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}} = \sqrt{\sum_{k \in I} {(F (k) - G (k))}^{2}}$
10	9	adantl	$⊢ ((I \in Fin \land F \in X \land G \in X) \land (x = F \land y = G)) \to \sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}} = \sqrt{\sum_{k \in I} {(F (k) - G (k))}^{2}}$
11		simp2	$⊢ (I \in Fin \land F \in X \land G \in X) \to F \in X$
12		simp3	$⊢ (I \in Fin \land F \in X \land G \in X) \to G \in X$
13		fvexd	$⊢ (I \in Fin \land F \in X \land G \in X) \to \sqrt{\sum_{k \in I} {(F (k) - G (k))}^{2}} \in V$
14	3 10 11 12 13	ovmpod	$⊢ (I \in Fin \land F \in X \land G \in X) \to F ℝ^{n} (I) G = \sqrt{\sum_{k \in I} {(F (k) - G (k))}^{2}}$

Metamath Proof Explorer