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	⊢ 𝐸 = ( 𝔼hil ‘ 1 )
	ehl1eudis.x	⊢ 𝑋 = ( ℝ ↑m { 1 } )
	ehl1eudis.d	⊢ 𝐷 = ( dist ‘ 𝐸 )
Assertion	ehl1eudisval	⊢ ( ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( 𝐹 𝐷 𝐺 ) = ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝐺 ‘ 1 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ehl1eudis.e	⊢ 𝐸 = ( 𝔼hil ‘ 1 )
2		ehl1eudis.x	⊢ 𝑋 = ( ℝ ↑m { 1 } )
3		ehl1eudis.d	⊢ 𝐷 = ( dist ‘ 𝐸 )
4		fveq1	⊢ ( 𝑥 = 𝐹 → ( 𝑥 ‘ 1 ) = ( 𝐹 ‘ 1 ) )
5	4	fvoveq1d	⊢ ( 𝑥 = 𝐹 → ( abs ‘ ( ( 𝑥 ‘ 1 ) − ( 𝑦 ‘ 1 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝑦 ‘ 1 ) ) ) )
6		fveq1	⊢ ( 𝑦 = 𝐺 → ( 𝑦 ‘ 1 ) = ( 𝐺 ‘ 1 ) )
7	6	oveq2d	⊢ ( 𝑦 = 𝐺 → ( ( 𝐹 ‘ 1 ) − ( 𝑦 ‘ 1 ) ) = ( ( 𝐹 ‘ 1 ) − ( 𝐺 ‘ 1 ) ) )
8	7	fveq2d	⊢ ( 𝑦 = 𝐺 → ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝑦 ‘ 1 ) ) ) = ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝐺 ‘ 1 ) ) ) )
9	1 2 3	ehl1eudis	⊢ 𝐷 = ( 𝑥 ∈ 𝑋 , 𝑦 ∈ 𝑋 ↦ ( abs ‘ ( ( 𝑥 ‘ 1 ) − ( 𝑦 ‘ 1 ) ) ) )
10		fvex	⊢ ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝐺 ‘ 1 ) ) ) ∈ V
11	5 8 9 10	ovmpo	⊢ ( ( 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋 ) → ( 𝐹 𝐷 𝐺 ) = ( abs ‘ ( ( 𝐹 ‘ 1 ) − ( 𝐺 ‘ 1 ) ) ) )