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

Proof

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