ehl1eudis

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

	Ref	Expression
Hypotheses	ehl1eudis.e	$⊢ E = 𝔼_{hil} (1)$
	ehl1eudis.x	$⊢ X = ℝ^{\{1\}}$
	ehl1eudis.d	$⊢ D = dist (E)$
Assertion	ehl1eudis	$⊢ D = (f \in X, g \in X ⟼ \|f (1) - g (1)\|)$

Proof

Step	Hyp	Ref	Expression
1		ehl1eudis.e	$⊢ E = 𝔼_{hil} (1)$
2		ehl1eudis.x	$⊢ X = ℝ^{\{1\}}$
3		ehl1eudis.d	$⊢ D = dist (E)$
4		1nn0	$⊢ 1 \in ℕ_{0}$
5		1z	$⊢ 1 \in ℤ$
6		fzsn	$⊢ 1 \in ℤ \to (1 \dots 1) = \{1\}$
7	5 6	ax-mp	$⊢ (1 \dots 1) = \{1\}$
8	7	eqcomi	$⊢ \{1\} = (1 \dots 1)$
9	8 1 2 3	ehleudis	$⊢ 1 \in ℕ_{0} \to D = (f \in X, g \in X ⟼ \sqrt{\sum_{k \in \{1\}} {(f (k) - g (k))}^{2}})$
10	4 9	ax-mp	$⊢ D = (f \in X, g \in X ⟼ \sqrt{\sum_{k \in \{1\}} {(f (k) - g (k))}^{2}})$
11	2	eleq2i	$⊢ f \in X \leftrightarrow f \in (ℝ^{\{1\}})$
12		reex	$⊢ ℝ \in V$
13		snex	$⊢ \{1\} \in V$
14	12 13	elmap	$⊢ f \in (ℝ^{\{1\}}) \leftrightarrow f : \{1\} ⟶ ℝ$
15	11 14	bitri	$⊢ f \in X \leftrightarrow f : \{1\} ⟶ ℝ$
16		id	$⊢ f : \{1\} ⟶ ℝ \to f : \{1\} ⟶ ℝ$
17		1ex	$⊢ 1 \in V$
18	17	snid	$⊢ 1 \in \{1\}$
19	18	a1i	$⊢ f : \{1\} ⟶ ℝ \to 1 \in \{1\}$
20	16 19	ffvelcdmd	$⊢ f : \{1\} ⟶ ℝ \to f (1) \in ℝ$
21	15 20	sylbi	$⊢ f \in X \to f (1) \in ℝ$
22	21	adantr	$⊢ (f \in X \land g \in X) \to f (1) \in ℝ$
23	2	eleq2i	$⊢ g \in X \leftrightarrow g \in (ℝ^{\{1\}})$
24	12 13	elmap	$⊢ g \in (ℝ^{\{1\}}) \leftrightarrow g : \{1\} ⟶ ℝ$
25	23 24	bitri	$⊢ g \in X \leftrightarrow g : \{1\} ⟶ ℝ$
26		id	$⊢ g : \{1\} ⟶ ℝ \to g : \{1\} ⟶ ℝ$
27	18	a1i	$⊢ g : \{1\} ⟶ ℝ \to 1 \in \{1\}$
28	26 27	ffvelcdmd	$⊢ g : \{1\} ⟶ ℝ \to g (1) \in ℝ$
29	25 28	sylbi	$⊢ g \in X \to g (1) \in ℝ$
30	29	adantl	$⊢ (f \in X \land g \in X) \to g (1) \in ℝ$
31	22 30	resubcld	$⊢ (f \in X \land g \in X) \to f (1) - g (1) \in ℝ$
32	31	resqcld	$⊢ (f \in X \land g \in X) \to {(f (1) - g (1))}^{2} \in ℝ$
33	32	recnd	$⊢ (f \in X \land g \in X) \to {(f (1) - g (1))}^{2} \in ℂ$
34		fveq2	$⊢ k = 1 \to f (k) = f (1)$
35		fveq2	$⊢ k = 1 \to g (k) = g (1)$
36	34 35	oveq12d	$⊢ k = 1 \to f (k) - g (k) = f (1) - g (1)$
37	36	oveq1d	$⊢ k = 1 \to {(f (k) - g (k))}^{2} = {(f (1) - g (1))}^{2}$
38	37	sumsn	$⊢ (1 \in ℤ \land {(f (1) - g (1))}^{2} \in ℂ) \to \sum_{k \in \{1\}} {(f (k) - g (k))}^{2} = {(f (1) - g (1))}^{2}$
39	5 33 38	sylancr	$⊢ (f \in X \land g \in X) \to \sum_{k \in \{1\}} {(f (k) - g (k))}^{2} = {(f (1) - g (1))}^{2}$
40	39	fveq2d	$⊢ (f \in X \land g \in X) \to \sqrt{\sum_{k \in \{1\}} {(f (k) - g (k))}^{2}} = \sqrt{{(f (1) - g (1))}^{2}}$
41	31	absred	$⊢ (f \in X \land g \in X) \to \|f (1) - g (1)\| = \sqrt{{(f (1) - g (1))}^{2}}$
42	40 41	eqtr4d	$⊢ (f \in X \land g \in X) \to \sqrt{\sum_{k \in \{1\}} {(f (k) - g (k))}^{2}} = \|f (1) - g (1)\|$
43	42	mpoeq3ia	$⊢ (f \in X, g \in X ⟼ \sqrt{\sum_{k \in \{1\}} {(f (k) - g (k))}^{2}}) = (f \in X, g \in X ⟼ \|f (1) - g (1)\|)$
44	10 43	eqtri	$⊢ D = (f \in X, g \in X ⟼ \|f (1) - g (1)\|)$

Metamath Proof Explorer

Theorem ehl1eudis

Proof