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 { 1 , 2 } )
	ehl2eudisval0.d	⊢ 𝐷 = ( dist ‘ 𝐸 )
	ehl2eudisval0.0	⊢ 0 = ( { 1 , 2 } × { 0 } )
Assertion	ehl2eudisval0	⊢ ( 𝐹 ∈ 𝑋 → ( 𝐹 𝐷 0 ) = ( √ ‘ ( ( ( 𝐹 ‘ 1 ) ↑ 2 ) + ( ( 𝐹 ‘ 2 ) ↑ 2 ) ) ) )

Proof

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