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}=⟨“00”⟩$$
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}=⟨“00”⟩$$
5		ovex	$$⊢\left(0..^2\right)\in \mathrm{V}$$
6		c0ex	$$⊢0\in \mathrm{V}$$
7		1ex	$$⊢1\in \mathrm{V}$$
8		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\}$$
9	6 7 6 8	mp3an	$$⊢\left\{0,1\right\}\times \left\{0\right\}=\left\{⟨0,0⟩,⟨1,0⟩\right\}$$
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		s2prop	$$⊢\left(0\in \mathrm{V}\wedge 0\in \mathrm{V}\right)\to ⟨“00”⟩=\left\{⟨0,0⟩,⟨1,0⟩\right\}$$
13	6 6 12	mp2an	$$⊢⟨“00”⟩=\left\{⟨0,0⟩,⟨1,0⟩\right\}$$
14	9 11 13	3eqtr4ri	$$⊢⟨“00”⟩=\left(0..^2\right)\times \left\{0\right\}$$
15	4 14	eqtri	$$⊢\underset{\dot{}}{0}=\left(0..^2\right)\times \left\{0\right\}$$
16	15 2	rrx0el	$$⊢\left(0..^2\right)\in \mathrm{V}\to \underset{\dot{}}{0}\in X$$
17	5 16	mp1i	$$⊢F\in X\to \underset{\dot{}}{0}\in X$$
18	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}$$
19	17 18	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}$$
20	4 13	eqtri	$$⊢\underset{\dot{}}{0}=\left\{⟨0,0⟩,⟨1,0⟩\right\}$$
21	20	fveq1i	$$⊢\underset{\dot{}}{0}\left(0\right)=\left\{⟨0,0⟩,⟨1,0⟩\right\}\left(0\right)$$
22		0ne1	$$⊢0\ne 1$$
23	6 6	fvpr1	$$⊢0\ne 1\to \left\{⟨0,0⟩,⟨1,0⟩\right\}\left(0\right)=0$$
24	22 23	ax-mp	$$⊢\left\{⟨0,0⟩,⟨1,0⟩\right\}\left(0\right)=0$$
25	21 24	eqtri	$$⊢\underset{\dot{}}{0}\left(0\right)=0$$
26	25	a1i	$$⊢F\in X\to \underset{\dot{}}{0}\left(0\right)=0$$
27	26	oveq2d	$$⊢F\in X\to F\left(0\right)-\underset{\dot{}}{0}\left(0\right)=F\left(0\right)-0$$
28		eqid	$$⊢\left(0..^2\right)=\left(0..^2\right)$$
29	28 2	rrx2pxel	$$⊢F\in X\to F\left(0\right)\in ℝ$$
30	29	recnd	$$⊢F\in X\to F\left(0\right)\in ℂ$$
31	30	subid1d	$$⊢F\in X\to F\left(0\right)-0=F\left(0\right)$$
32	27 31	eqtrd	$$⊢F\in X\to F\left(0\right)-\underset{\dot{}}{0}\left(0\right)=F\left(0\right)$$
33	32	oveq1d	$$⊢F\in X\to {\left(F\left(0\right)-\underset{\dot{}}{0}\left(0\right)\right)}^2={F\left(0\right)}^2$$
34	20	fveq1i	$$⊢\underset{\dot{}}{0}\left(1\right)=\left\{⟨0,0⟩,⟨1,0⟩\right\}\left(1\right)$$
35	7 6	fvpr2	$$⊢0\ne 1\to \left\{⟨0,0⟩,⟨1,0⟩\right\}\left(1\right)=0$$
36	22 35	mp1i	$$⊢F\in X\to \left\{⟨0,0⟩,⟨1,0⟩\right\}\left(1\right)=0$$
37	34 36	eqtrid	$$⊢F\in X\to \underset{\dot{}}{0}\left(1\right)=0$$
38	37	oveq2d	$$⊢F\in X\to F\left(1\right)-\underset{\dot{}}{0}\left(1\right)=F\left(1\right)-0$$
39	28 2	rrx2pyel	$$⊢F\in X\to F\left(1\right)\in ℝ$$
40	39	recnd	$$⊢F\in X\to F\left(1\right)\in ℂ$$
41	40	subid1d	$$⊢F\in X\to F\left(1\right)-0=F\left(1\right)$$
42	38 41	eqtrd	$$⊢F\in X\to F\left(1\right)-\underset{\dot{}}{0}\left(1\right)=F\left(1\right)$$
43	42	oveq1d	$$⊢F\in X\to {\left(F\left(1\right)-\underset{\dot{}}{0}\left(1\right)\right)}^2={F\left(1\right)}^2$$
44	33 43	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$$
45	44	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}$$
46	19 45	eqtrd	$$⊢F\in X\to FD\underset{\dot{}}{0}=\sqrt{{F\left(0\right)}^2+{F\left(1\right)}^2}$$