rrxdsfival

Description: The value of the Euclidean distance function in a generalized real Euclidean space of finite dimension. (Contributed by AV, 15-Jan-2023)

	Ref	Expression
Hypotheses	rrxdsfival.1	$⊢ X = ℝ^{I}$
	rrxdsfival.d	$⊢ D = dist (I)$
Assertion	rrxdsfival	$⊢ (I \in Fin \land F \in X \land G \in X) \to F D G = \sqrt{\sum_{k \in I} {(F (k) - G (k))}^{2}}$

Proof

Step	Hyp	Ref	Expression
1		rrxdsfival.1	$⊢ X = ℝ^{I}$
2		rrxdsfival.d	$⊢ D = dist (I)$
3		eqid	$⊢ I = I$
4	3 1	rrxdsfi	$⊢ I \in Fin \to dist (I) = (x \in X, y \in X ⟼ \sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}})$
5	2 4	syl5eq	$⊢ I \in Fin \to D = (x \in X, y \in X ⟼ \sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}})$
6	5	oveqd	$⊢ I \in Fin \to F D G = F (x \in X, y \in X ⟼ \sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}}) G$
7	6	3ad2ant1	$⊢ (I \in Fin \land F \in X \land G \in X) \to F D G = F (x \in X, y \in X ⟼ \sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}}) G$
8		eqidd	$⊢ (I \in Fin \land F \in X \land G \in X) \to (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}})$
9		fveq1	$⊢ x = F \to x (k) = F (k)$
10		fveq1	$⊢ y = G \to y (k) = G (k)$
11	9 10	oveqan12d	$⊢ (x = F \land y = G) \to x (k) - y (k) = F (k) - G (k)$
12	11	oveq1d	$⊢ (x = F \land y = G) \to {(x (k) - y (k))}^{2} = {(F (k) - G (k))}^{2}$
13	12	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}$
14	13	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}}$
15	14	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}}$
16		simp2	$⊢ (I \in Fin \land F \in X \land G \in X) \to F \in X$
17		simp3	$⊢ (I \in Fin \land F \in X \land G \in X) \to G \in X$
18		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$
19	8 15 16 17 18	ovmpod	$⊢ (I \in Fin \land F \in X \land G \in X) \to F (x \in X, y \in X ⟼ \sqrt{\sum_{k \in I} {(x (k) - y (k))}^{2}}) G = \sqrt{\sum_{k \in I} {(F (k) - G (k))}^{2}}$
20	7 19	eqtrd	$⊢ (I \in Fin \land F \in X \land G \in X) \to F D G = \sqrt{\sum_{k \in I} {(F (k) - G (k))}^{2}}$

Metamath Proof Explorer

Theorem rrxdsfival

Proof