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	⊢ 𝐸 = ( 𝔼_hil ‘ 1 )
	ehl1eudis.x	⊢ 𝑋 = ( ℝ ↑_m { 1 } )
	ehl1eudis.d	⊢ 𝐷 = ( dist ‘ 𝐸 )
Assertion	ehl1eudis	⊢ 𝐷 = ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( abs ‘ ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ehl1eudis.e	⊢ 𝐸 = ( 𝔼_hil ‘ 1 )
2		ehl1eudis.x	⊢ 𝑋 = ( ℝ ↑_m { 1 } )
3		ehl1eudis.d	⊢ 𝐷 = ( dist ‘ 𝐸 )
4		1nn0	⊢ 1 ∈ ℕ₀
5		1z	⊢ 1 ∈ ℤ
6		fzsn	⊢ ( 1 ∈ ℤ → ( 1 ... 1 ) = { 1 } )
7	5 6	ax-mp	⊢ ( 1 ... 1 ) = { 1 }
8	7	eqcomi	⊢ { 1 } = ( 1 ... 1 )
9	8 1 2 3	ehleudis	⊢ ( 1 ∈ ℕ₀ → 𝐷 = ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ { 1 } ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) )
10	4 9	ax-mp	⊢ 𝐷 = ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ { 1 } ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) )
11	2	eleq2i	⊢ ( 𝑓 ∈ 𝑋 ↔ 𝑓 ∈ ( ℝ ↑_m { 1 } ) )
12		reex	⊢ ℝ ∈ V
13		snex	⊢ { 1 } ∈ V
14	12 13	elmap	⊢ ( 𝑓 ∈ ( ℝ ↑_m { 1 } ) ↔ 𝑓 : { 1 } ⟶ ℝ )
15	11 14	bitri	⊢ ( 𝑓 ∈ 𝑋 ↔ 𝑓 : { 1 } ⟶ ℝ )
16		id	⊢ ( 𝑓 : { 1 } ⟶ ℝ → 𝑓 : { 1 } ⟶ ℝ )
17		1ex	⊢ 1 ∈ V
18	17	snid	⊢ 1 ∈ { 1 }
19	18	a1i	⊢ ( 𝑓 : { 1 } ⟶ ℝ → 1 ∈ { 1 } )
20	16 19	ffvelcdmd	⊢ ( 𝑓 : { 1 } ⟶ ℝ → ( 𝑓 ‘ 1 ) ∈ ℝ )
21	15 20	sylbi	⊢ ( 𝑓 ∈ 𝑋 → ( 𝑓 ‘ 1 ) ∈ ℝ )
22	21	adantr	⊢ ( ( 𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋 ) → ( 𝑓 ‘ 1 ) ∈ ℝ )
23	2	eleq2i	⊢ ( 𝑔 ∈ 𝑋 ↔ 𝑔 ∈ ( ℝ ↑_m { 1 } ) )
24	12 13	elmap	⊢ ( 𝑔 ∈ ( ℝ ↑_m { 1 } ) ↔ 𝑔 : { 1 } ⟶ ℝ )
25	23 24	bitri	⊢ ( 𝑔 ∈ 𝑋 ↔ 𝑔 : { 1 } ⟶ ℝ )
26		id	⊢ ( 𝑔 : { 1 } ⟶ ℝ → 𝑔 : { 1 } ⟶ ℝ )
27	18	a1i	⊢ ( 𝑔 : { 1 } ⟶ ℝ → 1 ∈ { 1 } )
28	26 27	ffvelcdmd	⊢ ( 𝑔 : { 1 } ⟶ ℝ → ( 𝑔 ‘ 1 ) ∈ ℝ )
29	25 28	sylbi	⊢ ( 𝑔 ∈ 𝑋 → ( 𝑔 ‘ 1 ) ∈ ℝ )
30	29	adantl	⊢ ( ( 𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋 ) → ( 𝑔 ‘ 1 ) ∈ ℝ )
31	22 30	resubcld	⊢ ( ( 𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋 ) → ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) ∈ ℝ )
32	31	resqcld	⊢ ( ( 𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋 ) → ( ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) ↑ 2 ) ∈ ℝ )
33	32	recnd	⊢ ( ( 𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋 ) → ( ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) ↑ 2 ) ∈ ℂ )
34		fveq2	⊢ ( 𝑘 = 1 → ( 𝑓 ‘ 𝑘 ) = ( 𝑓 ‘ 1 ) )
35		fveq2	⊢ ( 𝑘 = 1 → ( 𝑔 ‘ 𝑘 ) = ( 𝑔 ‘ 1 ) )
36	34 35	oveq12d	⊢ ( 𝑘 = 1 → ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) = ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) )
37	36	oveq1d	⊢ ( 𝑘 = 1 → ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) = ( ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) ↑ 2 ) )
38	37	sumsn	⊢ ( ( 1 ∈ ℤ ∧ ( ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) ↑ 2 ) ∈ ℂ ) → Σ 𝑘 ∈ { 1 } ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) = ( ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) ↑ 2 ) )
39	5 33 38	sylancr	⊢ ( ( 𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋 ) → Σ 𝑘 ∈ { 1 } ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) = ( ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) ↑ 2 ) )
40	39	fveq2d	⊢ ( ( 𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋 ) → ( √ ‘ Σ 𝑘 ∈ { 1 } ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) = ( √ ‘ ( ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) ↑ 2 ) ) )
41	31	absred	⊢ ( ( 𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋 ) → ( abs ‘ ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) ) = ( √ ‘ ( ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) ↑ 2 ) ) )
42	40 41	eqtr4d	⊢ ( ( 𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋 ) → ( √ ‘ Σ 𝑘 ∈ { 1 } ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) = ( abs ‘ ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) ) )
43	42	mpoeq3ia	⊢ ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( √ ‘ Σ 𝑘 ∈ { 1 } ( ( ( 𝑓 ‘ 𝑘 ) − ( 𝑔 ‘ 𝑘 ) ) ↑ 2 ) ) ) = ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( abs ‘ ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) ) )
44	10 43	eqtri	⊢ 𝐷 = ( 𝑓 ∈ 𝑋 , 𝑔 ∈ 𝑋 ↦ ( abs ‘ ( ( 𝑓 ‘ 1 ) − ( 𝑔 ‘ 1 ) ) ) )

Metamath Proof Explorer

Theorem ehl1eudis

Proof