ehl2eudisval

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

	Ref	Expression
Hypotheses	ehl2eudis.e	$⊢ E = 𝔼_{hil} (2)$
	ehl2eudis.x	$⊢ X = ℝ^{\{1, 2\}}$
	ehl2eudis.d	$⊢ D = dist (E)$
Assertion	ehl2eudisval	$⊢ (F \in X \land G \in X) \to F D G = \sqrt{{(F (1) - G (1))}^{2} + {(F (2) - G (2))}^{2}}$

Proof

Step	Hyp	Ref	Expression
1		ehl2eudis.e	$⊢ E = 𝔼_{hil} (2)$
2		ehl2eudis.x	$⊢ X = ℝ^{\{1, 2\}}$
3		ehl2eudis.d	$⊢ D = dist (E)$
4	1 2 3	ehl2eudis	$⊢ D = (f \in X, g \in X ⟼ \sqrt{{(f (1) - g (1))}^{2} + {(f (2) - g (2))}^{2}})$
5	4	oveqi	$⊢ F D G = F (f \in X, g \in X ⟼ \sqrt{{(f (1) - g (1))}^{2} + {(f (2) - g (2))}^{2}}) G$
6		eqidd	$⊢ (F \in X \land G \in X) \to (f \in X, g \in X ⟼ \sqrt{{(f (1) - g (1))}^{2} + {(f (2) - g (2))}^{2}}) = (f \in X, g \in X ⟼ \sqrt{{(f (1) - g (1))}^{2} + {(f (2) - g (2))}^{2}})$
7		fveq1	$⊢ f = F \to f (1) = F (1)$
8		fveq1	$⊢ g = G \to g (1) = G (1)$
9	7 8	oveqan12d	$⊢ (f = F \land g = G) \to f (1) - g (1) = F (1) - G (1)$
10	9	oveq1d	$⊢ (f = F \land g = G) \to {(f (1) - g (1))}^{2} = {(F (1) - G (1))}^{2}$
11		fveq1	$⊢ f = F \to f (2) = F (2)$
12		fveq1	$⊢ g = G \to g (2) = G (2)$
13	11 12	oveqan12d	$⊢ (f = F \land g = G) \to f (2) - g (2) = F (2) - G (2)$
14	13	oveq1d	$⊢ (f = F \land g = G) \to {(f (2) - g (2))}^{2} = {(F (2) - G (2))}^{2}$
15	10 14	oveq12d	$⊢ (f = F \land g = G) \to {(f (1) - g (1))}^{2} + {(f (2) - g (2))}^{2} = {(F (1) - G (1))}^{2} + {(F (2) - G (2))}^{2}$
16	15	fveq2d	$⊢ (f = F \land g = G) \to \sqrt{{(f (1) - g (1))}^{2} + {(f (2) - g (2))}^{2}} = \sqrt{{(F (1) - G (1))}^{2} + {(F (2) - G (2))}^{2}}$
17	16	adantl	$⊢ ((F \in X \land G \in X) \land (f = F \land g = G)) \to \sqrt{{(f (1) - g (1))}^{2} + {(f (2) - g (2))}^{2}} = \sqrt{{(F (1) - G (1))}^{2} + {(F (2) - G (2))}^{2}}$
18		simpl	$⊢ (F \in X \land G \in X) \to F \in X$
19		simpr	$⊢ (F \in X \land G \in X) \to G \in X$
20		fvexd	$⊢ (F \in X \land G \in X) \to \sqrt{{(F (1) - G (1))}^{2} + {(F (2) - G (2))}^{2}} \in V$
21	6 17 18 19 20	ovmpod	$⊢ (F \in X \land G \in X) \to F (f \in X, g \in X ⟼ \sqrt{{(f (1) - g (1))}^{2} + {(f (2) - g (2))}^{2}}) G = \sqrt{{(F (1) - G (1))}^{2} + {(F (2) - G (2))}^{2}}$
22	5 21	syl5eq	$⊢ (F \in X \land G \in X) \to F D G = \sqrt{{(F (1) - G (1))}^{2} + {(F (2) - G (2))}^{2}}$

Metamath Proof Explorer

Theorem ehl2eudisval

Proof