ehl2eudis - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > ehl2eudis		Structured version Visualization version GIF version

Theorem ehl2eudis 25636

Description: The Euclidean distance function in a real Euclidean space of dimension 2. (Contributed by AV, 16-Jan-2023.)

**Hypotheses**
Ref	Expression
ehl2eudis.e	⊢ 𝐸 = (𝔼_hil‘2)
ehl2eudis.x	⊢ 𝑋 = (ℝ ↑_m {1, 2})
ehl2eudis.d	⊢ 𝐷 = (dist‘𝐸)

**Assertion**
Ref	Expression
ehl2eudis	⊢ 𝐷 = (𝑓 ∈ 𝑋, 𝑔 ∈ 𝑋 ↦ (√‘((((𝑓‘1) − (𝑔‘1))↑2) + (((𝑓‘2) − (𝑔‘2))↑2))))

Distinct variable group: 𝑓,𝑔 Allowed substitution hints: 𝐷(𝑓, 𝑔) 𝐸(𝑓, 𝑔) 𝑋(𝑓, 𝑔)

Proof of Theorem ehl2eudis Dummy variable 𝑘 is distinct from all other variables.

Step	Hyp	Ref	Expression
1		2nn0 12540	. . 3 ⊢ 2 ∈ ℕ₀
2		fz12pr 13630	. . . . 5 ⊢ (1...2) = {1, 2}
3	2	eqcomi 2774	. . . 4 ⊢ {1, 2} = (1...2)
4		ehl2eudis.e	. . . 4 ⊢ 𝐸 = (𝔼_hil‘2)
5		ehl2eudis.x	. . . 4 ⊢ 𝑋 = (ℝ ↑_m {1, 2})
6		ehl2eudis.d	. . . 4 ⊢ 𝐷 = (dist‘𝐸)
7	3, 4, 5, 6	ehleudis 25632	. . 3 ⊢ (2 ∈ ℕ₀ → 𝐷 = (𝑓 ∈ 𝑋, 𝑔 ∈ 𝑋 ↦ (√‘Σ𝑘 ∈ {1, 2} (((𝑓‘𝑘) − (𝑔‘𝑘))↑2))))
8	1, 7	ax-mp 5	. 2 ⊢ 𝐷 = (𝑓 ∈ 𝑋, 𝑔 ∈ 𝑋 ↦ (√‘Σ𝑘 ∈ {1, 2} (((𝑓‘𝑘) − (𝑔‘𝑘))↑2)))
9		fveq2 6885	. . . . . . 7 ⊢ (𝑘 = 1 → (𝑓‘𝑘) = (𝑓‘1))
10		fveq2 6885	. . . . . . 7 ⊢ (𝑘 = 1 → (𝑔‘𝑘) = (𝑔‘1))
11	9, 10	oveq12d 7437	. . . . . 6 ⊢ (𝑘 = 1 → ((𝑓‘𝑘) − (𝑔‘𝑘)) = ((𝑓‘1) − (𝑔‘1)))
12	11	oveq1d 7434	. . . . 5 ⊢ (𝑘 = 1 → (((𝑓‘𝑘) − (𝑔‘𝑘))↑2) = (((𝑓‘1) − (𝑔‘1))↑2))
13		fveq2 6885	. . . . . . 7 ⊢ (𝑘 = 2 → (𝑓‘𝑘) = (𝑓‘2))
14		fveq2 6885	. . . . . . 7 ⊢ (𝑘 = 2 → (𝑔‘𝑘) = (𝑔‘2))
15	13, 14	oveq12d 7437	. . . . . 6 ⊢ (𝑘 = 2 → ((𝑓‘𝑘) − (𝑔‘𝑘)) = ((𝑓‘2) − (𝑔‘2)))
16	15	oveq1d 7434	. . . . 5 ⊢ (𝑘 = 2 → (((𝑓‘𝑘) − (𝑔‘𝑘))↑2) = (((𝑓‘2) − (𝑔‘2))↑2))
17	5	eleq2i 2857	. . . . . . . . . . . 12 ⊢ (𝑓 ∈ 𝑋 ↔ 𝑓 ∈ (ℝ ↑_m {1, 2}))
18		reex 11210	. . . . . . . . . . . . 13 ⊢ ℝ ∈ V
19		prex 5411	. . . . . . . . . . . . 13 ⊢ {1, 2} ∈ V
20	18, 19	elmap 8875	. . . . . . . . . . . 12 ⊢ (𝑓 ∈ (ℝ ↑_m {1, 2}) ↔ 𝑓:{1, 2}⟶ℝ)
21	17, 20	bitri 278	. . . . . . . . . . 11 ⊢ (𝑓 ∈ 𝑋 ↔ 𝑓:{1, 2}⟶ℝ)
22		id 23	. . . . . . . . . . . 12 ⊢ (𝑓:{1, 2}⟶ℝ → 𝑓:{1, 2}⟶ℝ)
23		1ex 11222	. . . . . . . . . . . . . 14 ⊢ 1 ∈ V
24	23	prid1 4730	. . . . . . . . . . . . 13 ⊢ 1 ∈ {1, 2}
25	24	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑓:{1, 2}⟶ℝ → 1 ∈ {1, 2})
26	22, 25	ffvelcdmd 7084	. . . . . . . . . . 11 ⊢ (𝑓:{1, 2}⟶ℝ → (𝑓‘1) ∈ ℝ)
27	21, 26	sylbi 220	. . . . . . . . . 10 ⊢ (𝑓 ∈ 𝑋 → (𝑓‘1) ∈ ℝ)
28	27	adantr 486	. . . . . . . . 9 ⊢ ((𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋) → (𝑓‘1) ∈ ℝ)
29	5	eleq2i 2857	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ 𝑋 ↔ 𝑔 ∈ (ℝ ↑_m {1, 2}))
30	18, 19	elmap 8875	. . . . . . . . . . . 12 ⊢ (𝑔 ∈ (ℝ ↑_m {1, 2}) ↔ 𝑔:{1, 2}⟶ℝ)
31	29, 30	bitri 278	. . . . . . . . . . 11 ⊢ (𝑔 ∈ 𝑋 ↔ 𝑔:{1, 2}⟶ℝ)
32		id 23	. . . . . . . . . . . 12 ⊢ (𝑔:{1, 2}⟶ℝ → 𝑔:{1, 2}⟶ℝ)
33	24	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑔:{1, 2}⟶ℝ → 1 ∈ {1, 2})
34	32, 33	ffvelcdmd 7084	. . . . . . . . . . 11 ⊢ (𝑔:{1, 2}⟶ℝ → (𝑔‘1) ∈ ℝ)
35	31, 34	sylbi 220	. . . . . . . . . 10 ⊢ (𝑔 ∈ 𝑋 → (𝑔‘1) ∈ ℝ)
36	35	adantl 487	. . . . . . . . 9 ⊢ ((𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋) → (𝑔‘1) ∈ ℝ)
37	28, 36	resubcld 11661	. . . . . . . 8 ⊢ ((𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋) → ((𝑓‘1) − (𝑔‘1)) ∈ ℝ)
38	37	resqcld 14183	. . . . . . 7 ⊢ ((𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋) → (((𝑓‘1) − (𝑔‘1))↑2) ∈ ℝ)
39	38	recnd 11256	. . . . . 6 ⊢ ((𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋) → (((𝑓‘1) − (𝑔‘1))↑2) ∈ ℂ)
40		2ex 12337	. . . . . . . . . . . . . 14 ⊢ 2 ∈ V
41	40	prid2 4731	. . . . . . . . . . . . 13 ⊢ 2 ∈ {1, 2}
42	41	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑓:{1, 2}⟶ℝ → 2 ∈ {1, 2})
43	22, 42	ffvelcdmd 7084	. . . . . . . . . . 11 ⊢ (𝑓:{1, 2}⟶ℝ → (𝑓‘2) ∈ ℝ)
44	21, 43	sylbi 220	. . . . . . . . . 10 ⊢ (𝑓 ∈ 𝑋 → (𝑓‘2) ∈ ℝ)
45	44	adantr 486	. . . . . . . . 9 ⊢ ((𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋) → (𝑓‘2) ∈ ℝ)
46	41	a1i 11	. . . . . . . . . . . 12 ⊢ (𝑔:{1, 2}⟶ℝ → 2 ∈ {1, 2})
47	32, 46	ffvelcdmd 7084	. . . . . . . . . . 11 ⊢ (𝑔:{1, 2}⟶ℝ → (𝑔‘2) ∈ ℝ)
48	31, 47	sylbi 220	. . . . . . . . . 10 ⊢ (𝑔 ∈ 𝑋 → (𝑔‘2) ∈ ℝ)
49	48	adantl 487	. . . . . . . . 9 ⊢ ((𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋) → (𝑔‘2) ∈ ℝ)
50	45, 49	resubcld 11661	. . . . . . . 8 ⊢ ((𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋) → ((𝑓‘2) − (𝑔‘2)) ∈ ℝ)
51	50	resqcld 14183	. . . . . . 7 ⊢ ((𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋) → (((𝑓‘2) − (𝑔‘2))↑2) ∈ ℝ)
52	51	recnd 11256	. . . . . 6 ⊢ ((𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋) → (((𝑓‘2) − (𝑔‘2))↑2) ∈ ℂ)
53	39, 52	jca 521	. . . . 5 ⊢ ((𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋) → ((((𝑓‘1) − (𝑔‘1))↑2) ∈ ℂ ∧ (((𝑓‘2) − (𝑔‘2))↑2) ∈ ℂ))
54	23, 40	pm3.2i 476	. . . . . 6 ⊢ (1 ∈ V ∧ 2 ∈ V)
55	54	a1i 11	. . . . 5 ⊢ ((𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋) → (1 ∈ V ∧ 2 ∈ V))
56		1ne2 12470	. . . . . 6 ⊢ 1 ≠ 2
57	56	a1i 11	. . . . 5 ⊢ ((𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋) → 1 ≠ 2)
58	12, 16, 53, 55, 57	sumpr 15826	. . . 4 ⊢ ((𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋) → Σ𝑘 ∈ {1, 2} (((𝑓‘𝑘) − (𝑔‘𝑘))↑2) = ((((𝑓‘1) − (𝑔‘1))↑2) + (((𝑓‘2) − (𝑔‘2))↑2)))
59	58	fveq2d 6889	. . 3 ⊢ ((𝑓 ∈ 𝑋 ∧ 𝑔 ∈ 𝑋) → (√‘Σ𝑘 ∈ {1, 2} (((𝑓‘𝑘) − (𝑔‘𝑘))↑2)) = (√‘((((𝑓‘1) − (𝑔‘1))↑2) + (((𝑓‘2) − (𝑔‘2))↑2))))
60	59	mpoeq3ia 7497	. 2 ⊢ (𝑓 ∈ 𝑋, 𝑔 ∈ 𝑋 ↦ (√‘Σ𝑘 ∈ {1, 2} (((𝑓‘𝑘) − (𝑔‘𝑘))↑2))) = (𝑓 ∈ 𝑋, 𝑔 ∈ 𝑋 ↦ (√‘((((𝑓‘1) − (𝑔‘1))↑2) + (((𝑓‘2) − (𝑔‘2))↑2))))
61	8, 60	eqtri 2788	1 ⊢ 𝐷 = (𝑓 ∈ 𝑋, 𝑔 ∈ 𝑋 ↦ (√‘((((𝑓‘1) − (𝑔‘1))↑2) + (((𝑓‘2) − (𝑔‘2))↑2))))

Colors of variables: wff setvar class

This proof depends on syntax axioms: ∧ wa 401 = wceq 1570 ∈ wcel 2146 ≠ wne 2960 Vcvv 3457 {cpr 4593 ⟶wf 6536 ‘cfv 6540 (class class class)co 7419 ∈ cmpo 7421 ↑_m cmap 8830 ℂcc 11117 ℝcr 11118 1c1 11120 + caddc 11122 − cmin 11460 2c2 12314 ℕ₀cn0 12523 ...cfz 13555 ↑cexp 14119 √csqrt 15312 Σcsu 15765 distcds 17345 𝔼_hilcehl 25598

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1943 ax-6 2000 ax-7 2041 ax-8 2148 ax-9 2156 ax-10 2179 ax-11 2195 ax-12 2216 ax-ext 2737 ax-rep 5240 ax-sep 5259 ax-nul 5271 ax-pow 5338 ax-pr 5406 ax-un 7742 ax-inf2 9617 ax-cnex 11175 ax-resscn 11176 ax-1cn 11177 ax-icn 11178 ax-addcl 11179 ax-addrcl 11180 ax-mulcl 11181 ax-mulrcl 11182 ax-mulcom 11183 ax-addass 11184 ax-mulass 11185 ax-distr 11186 ax-i2m1 11187 ax-1ne0 11188 ax-1rid 11189 ax-rnegex 11190 ax-rrecex 11191 ax-cnre 11192 ax-pre-lttri 11193 ax-pre-lttrn 11194 ax-pre-ltadd 11195 ax-pre-mulgt0 11196 ax-pre-sup 11197 ax-addf 11198 ax-mulf 11199

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2100 df-mo 2569 df-eu 2599 df-clab 2744 df-cleq 2757 df-clel 2840 df-nfc 2914 df-ne 2961 df-nel 3067 df-ral 3082 df-rex 3092 df-rmo 3371 df-reu 3372 df-rab 3419 df-v 3459 df-sbc 3747 df-csb 3855 df-dif 3909 df-un 3911 df-in 3913 df-ss 3923 df-pss 3926 df-nul 4287 df-if 4490 df-pw 4566 df-sn 4592 df-pr 4594 df-tp 4596 df-op 4598 df-uni 4875 df-int 4915 df-iun 4960 df-br 5112 df-opab 5176 df-mpt 5195 df-tr 5221 df-id 5558 df-eprel 5563 df-po 5571 df-so 5572 df-fr 5616 df-se 5617 df-we 5618 df-xp 5669 df-rel 5670 df-cnv 5671 df-co 5672 df-dm 5673 df-rn 5674 df-res 5675 df-ima 5676 df-pred 6306 df-ord 6367 df-on 6368 df-lim 6369 df-suc 6370 df-iota 6496 df-fun 6542 df-fn 6543 df-f 6544 df-f1 6545 df-fo 6546 df-f1o 6547 df-fv 6548 df-isom 6549 df-riota 7376 df-ov 7422 df-oprab 7423 df-mpo 7424 df-of 7684 df-om 7869 df-1st 7992 df-2nd 7993 df-supp 8163 df-tpos 8228 df-frecs 8284 df-wrecs 8315 df-recs 8364 df-rdg 8403 df-1o 8459 df-2o 8460 df-er 8700 df-map 8832 df-ixp 8902 df-en 8950 df-dom 8951 df-sdom 8952 df-fin 8953 df-fsupp 9329 df-sup 9409 df-oi 9479 df-card 9941 df-pnf 11264 df-mnf 11265 df-xr 11266 df-ltxr 11267 df-le 11268 df-sub 11462 df-neg 11463 df-div 11891 df-nn 12253 df-2 12322 df-3 12323 df-4 12324 df-5 12325 df-6 12326 df-7 12327 df-8 12328 df-9 12329 df-n0 12524 df-z 12611 df-dec 12732 df-uz 12883 df-rp 13037 df-fz 13556 df-fzo 13704 df-seq 14060 df-exp 14120 df-hash 14389 df-cj 15178 df-re 15179 df-im 15180 df-sqrt 15314 df-abs 15315 df-clim 15567 df-sum 15766 df-struct 17233 df-sets 17250 df-slot 17268 df-ndx 17280 df-base 17296 df-ress 17317 df-plusg 17349 df-mulr 17350 df-starv 17351 df-sca 17352 df-vsca 17353 df-ip 17354 df-tset 17355 df-ple 17356 df-ds 17358 df-unif 17359 df-hom 17360 df-cco 17361 df-0g 17520 df-gsum 17521 df-prds 17526 df-pws 17528 df-mgm 18724 df-sgrp 18813 df-mnd 18829 df-mhm 18882 df-grp 19051 df-minusg 19052 df-sbg 19053 df-subg 19237 df-ghm 19332 df-cntz 19435 df-cmn 19900 df-abl 19901 df-mgp 20265 df-rng 20279 df-ur 20312 df-ring 20365 df-cring 20366 df-oppr 20469 df-dvdsr 20489 df-unit 20490 df-invr 20520 df-dvr 20533 df-rhm 20604 df-subrng 20699 df-subrg 20723 df-drng 20883 df-field 20884 df-staf 20996 df-srng 20997 df-lmod 21037 df-lss 21107 df-sra 21348 df-rgmod 21349 df-cnfld 21577 df-refld 21809 df-dsmm 21936 df-frlm 21951 df-nm 24794 df-tng 24796 df-tcph 25383 df-rrx 25599 df-ehl 25600

This theorem is used by: ehl2eudisval 25637

W3C validator