Theorem ehl1eudisval

Description: The value of 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\{1\right\}}$$
	ehl1eudis.d	$$⊢D=\mathrm{dist}\left(E\right)$$
Assertion	ehl1eudisval	$$⊢\left(F\in X\wedge G\in X\right)\to FDG=\left|F\left(1\right)-G\left(1\right)\right|$$

Proof

Step	Hyp	Ref	Expression
1		ehl1eudis.e	$$⊢E={𝔼}_{\mathrm{hil}}\left(1\right)$$
2		ehl1eudis.x	$$⊢X={ℝ}^{\left\{1\right\}}$$
3		ehl1eudis.d	$$⊢D=\mathrm{dist}\left(E\right)$$
4		fveq1	$$⊢x=F\to x\left(1\right)=F\left(1\right)$$
5	4	fvoveq1d	$$⊢x=F\to \left|x\left(1\right)-y\left(1\right)\right|=\left|F\left(1\right)-y\left(1\right)\right|$$
6		fveq1	$$⊢y=G\to y\left(1\right)=G\left(1\right)$$
7	6	oveq2d	$$⊢y=G\to F\left(1\right)-y\left(1\right)=F\left(1\right)-G\left(1\right)$$
8	7	fveq2d	$$⊢y=G\to \left|F\left(1\right)-y\left(1\right)\right|=\left|F\left(1\right)-G\left(1\right)\right|$$
9	1 2 3	ehl1eudis	$$⊢D=\left(x\in X,y\in X⟼\left|x\left(1\right)-y\left(1\right)\right|\right)$$
10		fvex	$$⊢\left|F\left(1\right)-G\left(1\right)\right|\in \mathrm{V}$$
11	5 8 9 10	ovmpo	$$⊢\left(F\in X\wedge G\in X\right)\to FDG=\left|F\left(1\right)-G\left(1\right)\right|$$