Metamath Proof Explorer


Theorem ehleudisval

Description: The value of the Euclidean distance function in a real Euclidean space of finite dimension. (Contributed by AV, 15-Jan-2023)

Ref Expression
Hypotheses ehleudis.i I = 1 N
ehleudis.e E = 𝔼 hil N
ehleudis.x X = I
ehleudis.d D = dist E
Assertion ehleudisval N 0 F X G X F D G = k I F k G k 2

Proof

Step Hyp Ref Expression
1 ehleudis.i I = 1 N
2 ehleudis.e E = 𝔼 hil N
3 ehleudis.x X = I
4 ehleudis.d D = dist E
5 2 ehlval N 0 E = 1 N
6 5 fveq2d N 0 dist E = dist 1 N
7 4 6 syl5eq N 0 D = dist 1 N
8 7 oveqd N 0 F D G = F dist 1 N G
9 8 3ad2ant1 N 0 F X G X F D G = F dist 1 N G
10 fzfi 1 N Fin
11 1 10 eqeltri I Fin
12 3 eleq2i F X F I
13 12 biimpi F X F I
14 13 3ad2ant2 N 0 F X G X F I
15 3 eleq2i G X G I
16 15 biimpi G X G I
17 16 3ad2ant3 N 0 F X G X G I
18 eqid I = I
19 1 eqcomi 1 N = I
20 19 fveq2i 1 N = I
21 20 fveq2i dist 1 N = dist I
22 18 21 rrxdsfival I Fin F I G I F dist 1 N G = k I F k G k 2
23 11 14 17 22 mp3an2i N 0 F X G X F dist 1 N G = k I F k G k 2
24 9 23 eqtrd N 0 F X G X F D G = k I F k G k 2