Theorem ehl2eudis

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

	Ref	Expression
Hypotheses	ehl2eudis.e	$$⊢E={𝔼}_{\mathrm{hil}}\left(2\right)$$
	ehl2eudis.x	$$⊢X={ℝ}^{\left\{1,2\right\}}$$
	ehl2eudis.d	$$⊢D=\mathrm{dist}\left(E\right)$$
Assertion	ehl2eudis	$$⊢D=\left(f\in X,g\in X⟼\sqrt{{\left(f\left(1\right)-g\left(1\right)\right)}^2+{\left(f\left(2\right)-g\left(2\right)\right)}^2}\right)$$

Proof

Step	Hyp	Ref	Expression
1		ehl2eudis.e	$$⊢E={𝔼}_{\mathrm{hil}}\left(2\right)$$
2		ehl2eudis.x	$$⊢X={ℝ}^{\left\{1,2\right\}}$$
3		ehl2eudis.d	$$⊢D=\mathrm{dist}\left(E\right)$$
4		2nn0	$$⊢2\in {\mathbb{N}}_0$$
5		fz12pr	$$⊢\left(1\dots 2\right)=\left\{1,2\right\}$$
6	5	eqcomi	$$⊢\left\{1,2\right\}=\left(1\dots 2\right)$$
7	6 1 2 3	ehleudis	$$⊢2\in {\mathbb{N}}_0\to D=\left(f\in X,g\in X⟼\sqrt{\sum _{k\in \left\{1,2\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\{1,2\right\}}{\left(f\left(k\right)-g\left(k\right)\right)}^2}\right)$$
9		fveq2	$$⊢k=1\to f\left(k\right)=f\left(1\right)$$
10		fveq2	$$⊢k=1\to g\left(k\right)=g\left(1\right)$$
11	9 10	oveq12d	$$⊢k=1\to f\left(k\right)-g\left(k\right)=f\left(1\right)-g\left(1\right)$$
12	11	oveq1d	$$⊢k=1\to {\left(f\left(k\right)-g\left(k\right)\right)}^2={\left(f\left(1\right)-g\left(1\right)\right)}^2$$
13		fveq2	$$⊢k=2\to f\left(k\right)=f\left(2\right)$$
14		fveq2	$$⊢k=2\to g\left(k\right)=g\left(2\right)$$
15	13 14	oveq12d	$$⊢k=2\to f\left(k\right)-g\left(k\right)=f\left(2\right)-g\left(2\right)$$
16	15	oveq1d	$$⊢k=2\to {\left(f\left(k\right)-g\left(k\right)\right)}^2={\left(f\left(2\right)-g\left(2\right)\right)}^2$$
17	2	eleq2i	$$⊢f\in X\leftrightarrow f\in \left({ℝ}^{\left\{1,2\right\}}\right)$$
18		reex	$$⊢ℝ\in \mathrm{V}$$
19		prex	$$⊢\left\{1,2\right\}\in \mathrm{V}$$
20	18 19	elmap	$$⊢f\in \left({ℝ}^{\left\{1,2\right\}}\right)\leftrightarrow f:\left\{1,2\right\}⟶ℝ$$
21	17 20	bitri	$$⊢f\in X\leftrightarrow f:\left\{1,2\right\}⟶ℝ$$
22		id	$$⊢f:\left\{1,2\right\}⟶ℝ\to f:\left\{1,2\right\}⟶ℝ$$
23		1ex	$$⊢1\in \mathrm{V}$$
24	23	prid1	$$⊢1\in \left\{1,2\right\}$$
25	24	a1i	$$⊢f:\left\{1,2\right\}⟶ℝ\to 1\in \left\{1,2\right\}$$
26	22 25	ffvelrnd	$$⊢f:\left\{1,2\right\}⟶ℝ\to f\left(1\right)\in ℝ$$
27	21 26	sylbi	$$⊢f\in X\to f\left(1\right)\in ℝ$$
28	27	adantr	$$⊢\left(f\in X\wedge g\in X\right)\to f\left(1\right)\in ℝ$$
29	2	eleq2i	$$⊢g\in X\leftrightarrow g\in \left({ℝ}^{\left\{1,2\right\}}\right)$$
30	18 19	elmap	$$⊢g\in \left({ℝ}^{\left\{1,2\right\}}\right)\leftrightarrow g:\left\{1,2\right\}⟶ℝ$$
31	29 30	bitri	$$⊢g\in X\leftrightarrow g:\left\{1,2\right\}⟶ℝ$$
32		id	$$⊢g:\left\{1,2\right\}⟶ℝ\to g:\left\{1,2\right\}⟶ℝ$$
33	24	a1i	$$⊢g:\left\{1,2\right\}⟶ℝ\to 1\in \left\{1,2\right\}$$
34	32 33	ffvelrnd	$$⊢g:\left\{1,2\right\}⟶ℝ\to g\left(1\right)\in ℝ$$
35	31 34	sylbi	$$⊢g\in X\to g\left(1\right)\in ℝ$$
36	35	adantl	$$⊢\left(f\in X\wedge g\in X\right)\to g\left(1\right)\in ℝ$$
37	28 36	resubcld	$$⊢\left(f\in X\wedge g\in X\right)\to f\left(1\right)-g\left(1\right)\in ℝ$$
38	37	resqcld	$$⊢\left(f\in X\wedge g\in X\right)\to {\left(f\left(1\right)-g\left(1\right)\right)}^2\in ℝ$$
39	38	recnd	$$⊢\left(f\in X\wedge g\in X\right)\to {\left(f\left(1\right)-g\left(1\right)\right)}^2\in ℂ$$
40		2ex	$$⊢2\in \mathrm{V}$$
41	40	prid2	$$⊢2\in \left\{1,2\right\}$$
42	41	a1i	$$⊢f:\left\{1,2\right\}⟶ℝ\to 2\in \left\{1,2\right\}$$
43	22 42	ffvelrnd	$$⊢f:\left\{1,2\right\}⟶ℝ\to f\left(2\right)\in ℝ$$
44	21 43	sylbi	$$⊢f\in X\to f\left(2\right)\in ℝ$$
45	44	adantr	$$⊢\left(f\in X\wedge g\in X\right)\to f\left(2\right)\in ℝ$$
46	41	a1i	$$⊢g:\left\{1,2\right\}⟶ℝ\to 2\in \left\{1,2\right\}$$
47	32 46	ffvelrnd	$$⊢g:\left\{1,2\right\}⟶ℝ\to g\left(2\right)\in ℝ$$
48	31 47	sylbi	$$⊢g\in X\to g\left(2\right)\in ℝ$$
49	48	adantl	$$⊢\left(f\in X\wedge g\in X\right)\to g\left(2\right)\in ℝ$$
50	45 49	resubcld	$$⊢\left(f\in X\wedge g\in X\right)\to f\left(2\right)-g\left(2\right)\in ℝ$$
51	50	resqcld	$$⊢\left(f\in X\wedge g\in X\right)\to {\left(f\left(2\right)-g\left(2\right)\right)}^2\in ℝ$$
52	51	recnd	$$⊢\left(f\in X\wedge g\in X\right)\to {\left(f\left(2\right)-g\left(2\right)\right)}^2\in ℂ$$
53	39 52	jca	$$⊢\left(f\in X\wedge g\in X\right)\to \left({\left(f\left(1\right)-g\left(1\right)\right)}^2\in ℂ\wedge {\left(f\left(2\right)-g\left(2\right)\right)}^2\in ℂ\right)$$
54	23 40	pm3.2i	$$⊢\left(1\in \mathrm{V}\wedge 2\in \mathrm{V}\right)$$
55	54	a1i	$$⊢\left(f\in X\wedge g\in X\right)\to \left(1\in \mathrm{V}\wedge 2\in \mathrm{V}\right)$$
56		1ne2	$$⊢1\ne 2$$
57	56	a1i	$$⊢\left(f\in X\wedge g\in X\right)\to 1\ne 2$$
58	12 16 53 55 57	sumpr	$$⊢\left(f\in X\wedge g\in X\right)\to \sum _{k\in \left\{1,2\right\}}{\left(f\left(k\right)-g\left(k\right)\right)}^2={\left(f\left(1\right)-g\left(1\right)\right)}^2+{\left(f\left(2\right)-g\left(2\right)\right)}^2$$
59	58	fveq2d	$$⊢\left(f\in X\wedge g\in X\right)\to \sqrt{\sum _{k\in \left\{1,2\right\}}{\left(f\left(k\right)-g\left(k\right)\right)}^2}=\sqrt{{\left(f\left(1\right)-g\left(1\right)\right)}^2+{\left(f\left(2\right)-g\left(2\right)\right)}^2}$$
60	59	mpoeq3ia	$$⊢\left(f\in X,g\in X⟼\sqrt{\sum _{k\in \left\{1,2\right\}}{\left(f\left(k\right)-g\left(k\right)\right)}^2}\right)=\left(f\in X,g\in X⟼\sqrt{{\left(f\left(1\right)-g\left(1\right)\right)}^2+{\left(f\left(2\right)-g\left(2\right)\right)}^2}\right)$$
61	8 60	eqtri	$$⊢D=\left(f\in X,g\in X⟼\sqrt{{\left(f\left(1\right)-g\left(1\right)\right)}^2+{\left(f\left(2\right)-g\left(2\right)\right)}^2}\right)$$