Theorem ehl2eudisval0

Description: The Euclidean distance of a point to the origin in a real Euclidean space of dimension 2. (Contributed by AV, 26-Feb-2023)

	Ref	Expression
Hypotheses	ehl2eudisval0.e	⊢ 𝐸 = ( 𝔼hil ‘ 2 )
	ehl2eudisval0.x	⊢ 𝑋 = ( ℝ ↑m ( 0 ..^ 2 ) )
	ehl2eudisval0.d	⊢ 𝐷 = ( dist ‘ 𝐸 )
	ehl2eudisval0.0	⊢ 0 = ⟨“ 0 0 ”⟩
Assertion	ehl2eudisval0	⊢ ( 𝐹 ∈ 𝑋 → ( 𝐹 𝐷 0 ) = ( √ ‘ ( ( ( 𝐹 ‘ 0 ) ↑ 2 ) + ( ( 𝐹 ‘ 1 ) ↑ 2 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ehl2eudisval0.e	⊢ 𝐸 = ( 𝔼hil ‘ 2 )
2		ehl2eudisval0.x	⊢ 𝑋 = ( ℝ ↑m ( 0 ..^ 2 ) )
3		ehl2eudisval0.d	⊢ 𝐷 = ( dist ‘ 𝐸 )
4		ehl2eudisval0.0	⊢ 0 = ⟨“ 0 0 ”⟩
5		ovex	⊢ ( 0 ..^ 2 ) ∈ V
6		c0ex	⊢ 0 ∈ V
7		1ex	⊢ 1 ∈ V
8		xpprsng	⊢ ( ( 0 ∈ V ∧ 1 ∈ V ∧ 0 ∈ V ) → ( { 0 , 1 } × { 0 } ) = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } )
9	6 7 6 8	mp3an	⊢ ( { 0 , 1 } × { 0 } ) = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ }
10		fzo0to2pr	⊢ ( 0 ..^ 2 ) = { 0 , 1 }
11	10	xpeq1i	⊢ ( ( 0 ..^ 2 ) × { 0 } ) = ( { 0 , 1 } × { 0 } )
12		s2prop	⊢ ( ( 0 ∈ V ∧ 0 ∈ V ) → ⟨“ 0 0 ”⟩ = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } )
13	6 6 12	mp2an	⊢ ⟨“ 0 0 ”⟩ = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ }
14	9 11 13	3eqtr4ri	⊢ ⟨“ 0 0 ”⟩ = ( ( 0 ..^ 2 ) × { 0 } )
15	4 14	eqtri	⊢ 0 = ( ( 0 ..^ 2 ) × { 0 } )
16	15 2	rrx0el	⊢ ( ( 0 ..^ 2 ) ∈ V → 0 ∈ 𝑋 )
17	5 16	mp1i	⊢ ( 𝐹 ∈ 𝑋 → 0 ∈ 𝑋 )
18	1 2 3	ehl2eudisval	⊢ ( ( 𝐹 ∈ 𝑋 ∧ 0 ∈ 𝑋 ) → ( 𝐹 𝐷 0 ) = ( √ ‘ ( ( ( ( 𝐹 ‘ 0 ) − ( 0 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝐹 ‘ 1 ) − ( 0 ‘ 1 ) ) ↑ 2 ) ) ) )
19	17 18	mpdan	⊢ ( 𝐹 ∈ 𝑋 → ( 𝐹 𝐷 0 ) = ( √ ‘ ( ( ( ( 𝐹 ‘ 0 ) − ( 0 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝐹 ‘ 1 ) − ( 0 ‘ 1 ) ) ↑ 2 ) ) ) )
20	4 13	eqtri	⊢ 0 = { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ }
21	20	fveq1i	⊢ ( 0 ‘ 0 ) = ( { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } ‘ 0 )
22		0ne1	⊢ 0 ≠ 1
23	6 6	fvpr1	⊢ ( 0 ≠ 1 → ( { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } ‘ 0 ) = 0 )
24	22 23	ax-mp	⊢ ( { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } ‘ 0 ) = 0
25	21 24	eqtri	⊢ ( 0 ‘ 0 ) = 0
26	25	a1i	⊢ ( 𝐹 ∈ 𝑋 → ( 0 ‘ 0 ) = 0 )
27	26	oveq2d	⊢ ( 𝐹 ∈ 𝑋 → ( ( 𝐹 ‘ 0 ) − ( 0 ‘ 0 ) ) = ( ( 𝐹 ‘ 0 ) − 0 ) )
28		eqid	⊢ ( 0 ..^ 2 ) = ( 0 ..^ 2 )
29	28 2	rrx2pxel	⊢ ( 𝐹 ∈ 𝑋 → ( 𝐹 ‘ 0 ) ∈ ℝ )
30	29	recnd	⊢ ( 𝐹 ∈ 𝑋 → ( 𝐹 ‘ 0 ) ∈ ℂ )
31	30	subid1d	⊢ ( 𝐹 ∈ 𝑋 → ( ( 𝐹 ‘ 0 ) − 0 ) = ( 𝐹 ‘ 0 ) )
32	27 31	eqtrd	⊢ ( 𝐹 ∈ 𝑋 → ( ( 𝐹 ‘ 0 ) − ( 0 ‘ 0 ) ) = ( 𝐹 ‘ 0 ) )
33	32	oveq1d	⊢ ( 𝐹 ∈ 𝑋 → ( ( ( 𝐹 ‘ 0 ) − ( 0 ‘ 0 ) ) ↑ 2 ) = ( ( 𝐹 ‘ 0 ) ↑ 2 ) )
34	20	fveq1i	⊢ ( 0 ‘ 1 ) = ( { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } ‘ 1 )
35	7 6	fvpr2	⊢ ( 0 ≠ 1 → ( { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } ‘ 1 ) = 0 )
36	22 35	mp1i	⊢ ( 𝐹 ∈ 𝑋 → ( { ⟨ 0 , 0 ⟩ , ⟨ 1 , 0 ⟩ } ‘ 1 ) = 0 )
37	34 36	eqtrid	⊢ ( 𝐹 ∈ 𝑋 → ( 0 ‘ 1 ) = 0 )
38	37	oveq2d	⊢ ( 𝐹 ∈ 𝑋 → ( ( 𝐹 ‘ 1 ) − ( 0 ‘ 1 ) ) = ( ( 𝐹 ‘ 1 ) − 0 ) )
39	28 2	rrx2pyel	⊢ ( 𝐹 ∈ 𝑋 → ( 𝐹 ‘ 1 ) ∈ ℝ )
40	39	recnd	⊢ ( 𝐹 ∈ 𝑋 → ( 𝐹 ‘ 1 ) ∈ ℂ )
41	40	subid1d	⊢ ( 𝐹 ∈ 𝑋 → ( ( 𝐹 ‘ 1 ) − 0 ) = ( 𝐹 ‘ 1 ) )
42	38 41	eqtrd	⊢ ( 𝐹 ∈ 𝑋 → ( ( 𝐹 ‘ 1 ) − ( 0 ‘ 1 ) ) = ( 𝐹 ‘ 1 ) )
43	42	oveq1d	⊢ ( 𝐹 ∈ 𝑋 → ( ( ( 𝐹 ‘ 1 ) − ( 0 ‘ 1 ) ) ↑ 2 ) = ( ( 𝐹 ‘ 1 ) ↑ 2 ) )
44	33 43	oveq12d	⊢ ( 𝐹 ∈ 𝑋 → ( ( ( ( 𝐹 ‘ 0 ) − ( 0 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝐹 ‘ 1 ) − ( 0 ‘ 1 ) ) ↑ 2 ) ) = ( ( ( 𝐹 ‘ 0 ) ↑ 2 ) + ( ( 𝐹 ‘ 1 ) ↑ 2 ) ) )
45	44	fveq2d	⊢ ( 𝐹 ∈ 𝑋 → ( √ ‘ ( ( ( ( 𝐹 ‘ 0 ) − ( 0 ‘ 0 ) ) ↑ 2 ) + ( ( ( 𝐹 ‘ 1 ) − ( 0 ‘ 1 ) ) ↑ 2 ) ) ) = ( √ ‘ ( ( ( 𝐹 ‘ 0 ) ↑ 2 ) + ( ( 𝐹 ‘ 1 ) ↑ 2 ) ) ) )
46	19 45	eqtrd	⊢ ( 𝐹 ∈ 𝑋 → ( 𝐹 𝐷 0 ) = ( √ ‘ ( ( ( 𝐹 ‘ 0 ) ↑ 2 ) + ( ( 𝐹 ‘ 1 ) ↑ 2 ) ) ) )