Theorem 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={𝔼}_{\mathrm{hil}}\left(1\right)$$
	ehl1eudis.x	$$⊢X={ℝ}^{\left\{0\right\}}$$
	ehl1eudis.d	$$⊢D=\mathrm{dist}\left(E\right)$$
Assertion	ehl1eudis	$$⊢D=\left(f\in X,g\in X⟼\left|f\left(0\right)-g\left(0\right)\right|\right)$$

Proof

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