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	$$⊢E={𝔼}_{\mathrm{hil}}\left(2\right)$$
	ehl2eudisval0.x	$$⊢X={ℝ}^{\left(0..^2\right)}$$
	ehl2eudisval0.d	$$⊢D=\mathrm{dist}\left(E\right)$$
	ehl2eudisval0.0	$$⊢\underset{\dot{}}{0}=\left(0..^2\right)\times \left\{0\right\}$$
Assertion	ehl2eudisval0	$$⊢F\in X\to FD\underset{\dot{}}{0}=\sqrt{{F\left(0\right)}^2+{F\left(1\right)}^2}$$

Proof

Step	Hyp	Ref	Expression
1		ehl2eudisval0.e	$$⊢E={𝔼}_{\mathrm{hil}}\left(2\right)$$
2		ehl2eudisval0.x	$$⊢X={ℝ}^{\left(0..^2\right)}$$
3		ehl2eudisval0.d	$$⊢D=\mathrm{dist}\left(E\right)$$
4		ehl2eudisval0.0	$$⊢\underset{\dot{}}{0}=\left(0..^2\right)\times \left\{0\right\}$$
5		ovex	$$⊢\left(0..^2\right)\in \mathrm{V}$$
6	4 2	rrx0el	$$⊢\left(0..^2\right)\in \mathrm{V}\to \underset{\dot{}}{0}\in X$$
7	5 6	mp1i	$$⊢F\in X\to \underset{\dot{}}{0}\in X$$
8	1 2 3	ehl2eudisval	$$⊢\left(F\in X\wedge \underset{\dot{}}{0}\in X\right)\to FD\underset{\dot{}}{0}=\sqrt{{\left(F\left(0\right)-\underset{\dot{}}{0}\left(0\right)\right)}^2+{\left(F\left(1\right)-\underset{\dot{}}{0}\left(1\right)\right)}^2}$$
9	7 8	mpdan	$$⊢F\in X\to FD\underset{\dot{}}{0}=\sqrt{{\left(F\left(0\right)-\underset{\dot{}}{0}\left(0\right)\right)}^2+{\left(F\left(1\right)-\underset{\dot{}}{0}\left(1\right)\right)}^2}$$
10		fzo0to2pr	$$⊢\left(0..^2\right)=\left\{0,1\right\}$$
11	10	xpeq1i	$$⊢\left(0..^2\right)\times \left\{0\right\}=\left\{0,1\right\}\times \left\{0\right\}$$
12		c0ex	$$⊢0\in \mathrm{V}$$
13		1ex	$$⊢1\in \mathrm{V}$$
14		xpprsng	$$⊢\left(0\in \mathrm{V}\wedge 1\in \mathrm{V}\wedge 0\in \mathrm{V}\right)\to \left\{0,1\right\}\times \left\{0\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}$$
15	12 13 12 14	mp3an	$$⊢\left\{0,1\right\}\times \left\{0\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}$$
16	4 11 15	3eqtri	$$⊢\underset{\dot{}}{0}=\left\{⟨0,0⟩,⟨1,0⟩\right\}$$
17	16	fveq1i	$$⊢\underset{\dot{}}{0}\left(0\right)=\left\{⟨0,0⟩,⟨1,0⟩\right\}\left(0\right)$$
18		0ne1	$$⊢0\ne 1$$
19	12 12	fvpr1	$$⊢0\ne 1\to \left\{⟨0,0⟩,⟨1,0⟩\right\}\left(0\right)=0$$
20	18 19	ax-mp	$$⊢\left\{⟨0,0⟩,⟨1,0⟩\right\}\left(0\right)=0$$
21	17 20	eqtri	$$⊢\underset{\dot{}}{0}\left(0\right)=0$$
22	21	a1i	$$⊢F\in X\to \underset{\dot{}}{0}\left(0\right)=0$$
23	22	oveq2d	$$⊢F\in X\to F\left(0\right)-\underset{\dot{}}{0}\left(0\right)=F\left(0\right)-0$$
24		eqid	$$⊢\left(0..^2\right)=\left(0..^2\right)$$
25	24 2	rrx2pxel	$$⊢F\in X\to F\left(0\right)\in ℝ$$
26	25	recnd	$$⊢F\in X\to F\left(0\right)\in ℂ$$
27	26	subid1d	$$⊢F\in X\to F\left(0\right)-0=F\left(0\right)$$
28	23 27	eqtrd	$$⊢F\in X\to F\left(0\right)-\underset{\dot{}}{0}\left(0\right)=F\left(0\right)$$
29	28	oveq1d	$$⊢F\in X\to {\left(F\left(0\right)-\underset{\dot{}}{0}\left(0\right)\right)}^2={F\left(0\right)}^2$$
30	16	fveq1i	$$⊢\underset{\dot{}}{0}\left(1\right)=\left\{⟨0,0⟩,⟨1,0⟩\right\}\left(1\right)$$
31	13 12	fvpr2	$$⊢0\ne 1\to \left\{⟨0,0⟩,⟨1,0⟩\right\}\left(1\right)=0$$
32	18 31	mp1i	$$⊢F\in X\to \left\{⟨0,0⟩,⟨1,0⟩\right\}\left(1\right)=0$$
33	30 32	eqtrid	$$⊢F\in X\to \underset{\dot{}}{0}\left(1\right)=0$$
34	33	oveq2d	$$⊢F\in X\to F\left(1\right)-\underset{\dot{}}{0}\left(1\right)=F\left(1\right)-0$$
35	24 2	rrx2pyel	$$⊢F\in X\to F\left(1\right)\in ℝ$$
36	35	recnd	$$⊢F\in X\to F\left(1\right)\in ℂ$$
37	36	subid1d	$$⊢F\in X\to F\left(1\right)-0=F\left(1\right)$$
38	34 37	eqtrd	$$⊢F\in X\to F\left(1\right)-\underset{\dot{}}{0}\left(1\right)=F\left(1\right)$$
39	38	oveq1d	$$⊢F\in X\to {\left(F\left(1\right)-\underset{\dot{}}{0}\left(1\right)\right)}^2={F\left(1\right)}^2$$
40	29 39	oveq12d	$$⊢F\in X\to {\left(F\left(0\right)-\underset{\dot{}}{0}\left(0\right)\right)}^2+{\left(F\left(1\right)-\underset{\dot{}}{0}\left(1\right)\right)}^2={F\left(0\right)}^2+{F\left(1\right)}^2$$
41	40	fveq2d	$$⊢F\in X\to \sqrt{{\left(F\left(0\right)-\underset{\dot{}}{0}\left(0\right)\right)}^2+{\left(F\left(1\right)-\underset{\dot{}}{0}\left(1\right)\right)}^2}=\sqrt{{F\left(0\right)}^2+{F\left(1\right)}^2}$$
42	9 41	eqtrd	$$⊢F\in X\to FD\underset{\dot{}}{0}=\sqrt{{F\left(0\right)}^2+{F\left(1\right)}^2}$$