Metamath Proof Explorer


Theorem rrxmval

Description: The value of the Euclidean metric. Compare with rrnmval . (Contributed by Thierry Arnoux, 30-Jun-2019)

Ref Expression
Hypotheses rrxmval.1 X = h I | finSupp 0 h
rrxmval.d D = dist I
Assertion rrxmval I V F X G X F D G = k supp 0 F supp 0 G F k G k 2

Proof

Step Hyp Ref Expression
1 rrxmval.1 X = h I | finSupp 0 h
2 rrxmval.d D = dist I
3 eqid I = I
4 eqid Base I = Base I
5 3 4 rrxds I V f Base I , g Base I fld x I f x g x 2 = dist I
6 5 2 syl6reqr I V D = f Base I , g Base I fld x I f x g x 2
7 3 4 rrxbase I V Base I = h I | finSupp 0 h
8 7 1 syl6reqr I V X = Base I
9 mpoeq12 X = Base I X = Base I f X , g X fld x I f x g x 2 = f Base I , g Base I fld x I f x g x 2
10 8 8 9 syl2anc I V f X , g X fld x I f x g x 2 = f Base I , g Base I fld x I f x g x 2
11 6 10 eqtr4d I V D = f X , g X fld x I f x g x 2
12 11 3ad2ant1 I V F X G X D = f X , g X fld x I f x g x 2
13 simprl I V F X G X f = F g = G f = F
14 13 fveq1d I V F X G X f = F g = G f x = F x
15 simprr I V F X G X f = F g = G g = G
16 15 fveq1d I V F X G X f = F g = G g x = G x
17 14 16 oveq12d I V F X G X f = F g = G f x g x = F x G x
18 17 oveq1d I V F X G X f = F g = G f x g x 2 = F x G x 2
19 18 mpteq2dv I V F X G X f = F g = G x I f x g x 2 = x I F x G x 2
20 19 oveq2d I V F X G X f = F g = G fld x I f x g x 2 = fld x I F x G x 2
21 simp2 I V F X G X F X
22 1 21 rrxf I V F X G X F : I
23 22 ffvelrnda I V F X G X x I F x
24 simp3 I V F X G X G X
25 1 24 rrxf I V F X G X G : I
26 25 ffvelrnda I V F X G X x I G x
27 23 26 resubcld I V F X G X x I F x G x
28 27 resqcld I V F X G X x I F x G x 2
29 28 fmpttd I V F X G X x I F x G x 2 : I
30 1 21 rrxfsupp I V F X G X F supp 0 Fin
31 1 24 rrxfsupp I V F X G X G supp 0 Fin
32 unfi F supp 0 Fin G supp 0 Fin supp 0 F supp 0 G Fin
33 30 31 32 syl2anc I V F X G X supp 0 F supp 0 G Fin
34 1 rrxmvallem I V F X G X x I F x G x 2 supp 0 supp 0 F supp 0 G
35 33 34 ssfid I V F X G X x I F x G x 2 supp 0 Fin
36 mptexg I V x I F x G x 2 V
37 funmpt Fun x I F x G x 2
38 0cn 0
39 funisfsupp Fun x I F x G x 2 x I F x G x 2 V 0 finSupp 0 x I F x G x 2 x I F x G x 2 supp 0 Fin
40 37 38 39 mp3an13 x I F x G x 2 V finSupp 0 x I F x G x 2 x I F x G x 2 supp 0 Fin
41 36 40 syl I V finSupp 0 x I F x G x 2 x I F x G x 2 supp 0 Fin
42 41 3ad2ant1 I V F X G X finSupp 0 x I F x G x 2 x I F x G x 2 supp 0 Fin
43 35 42 mpbird I V F X G X finSupp 0 x I F x G x 2
44 simp1 I V F X G X I V
45 regsumsupp x I F x G x 2 : I finSupp 0 x I F x G x 2 I V fld x I F x G x 2 = k x I F x G x 2 supp 0 x I F x G x 2 k
46 29 43 44 45 syl3anc I V F X G X fld x I F x G x 2 = k x I F x G x 2 supp 0 x I F x G x 2 k
47 suppssdm x I F x G x 2 supp 0 dom x I F x G x 2
48 eqid x I F x G x 2 = x I F x G x 2
49 48 dmmptss dom x I F x G x 2 I
50 47 49 sstri x I F x G x 2 supp 0 I
51 50 a1i I V F X G X x I F x G x 2 supp 0 I
52 51 sselda I V F X G X k supp 0 x I F x G x 2 k I
53 eqidd I V F X G X k I x I F x G x 2 = x I F x G x 2
54 simpr I V F X G X k I x = k x = k
55 54 fveq2d I V F X G X k I x = k F x = F k
56 54 fveq2d I V F X G X k I x = k G x = G k
57 55 56 oveq12d I V F X G X k I x = k F x G x = F k G k
58 57 oveq1d I V F X G X k I x = k F x G x 2 = F k G k 2
59 simpr I V F X G X k I k I
60 ovexd I V F X G X k I F k G k 2 V
61 53 58 59 60 fvmptd I V F X G X k I x I F x G x 2 k = F k G k 2
62 61 eqcomd I V F X G X k I F k G k 2 = x I F x G x 2 k
63 52 62 syldan I V F X G X k supp 0 x I F x G x 2 F k G k 2 = x I F x G x 2 k
64 63 sumeq2dv I V F X G X k x I F x G x 2 supp 0 F k G k 2 = k x I F x G x 2 supp 0 x I F x G x 2 k
65 46 64 eqtr4d I V F X G X fld x I F x G x 2 = k x I F x G x 2 supp 0 F k G k 2
66 65 adantr I V F X G X f = F g = G fld x I F x G x 2 = k x I F x G x 2 supp 0 F k G k 2
67 22 ffvelrnda I V F X G X k I F k
68 67 recnd I V F X G X k I F k
69 25 ffvelrnda I V F X G X k I G k
70 69 recnd I V F X G X k I G k
71 68 70 subcld I V F X G X k I F k G k
72 71 sqcld I V F X G X k I F k G k 2
73 52 72 syldan I V F X G X k supp 0 x I F x G x 2 F k G k 2
74 1 21 rrxsuppss I V F X G X F supp 0 I
75 1 24 rrxsuppss I V F X G X G supp 0 I
76 74 75 unssd I V F X G X supp 0 F supp 0 G I
77 76 ssdifssd I V F X G X supp 0 F supp 0 G supp 0 x I F x G x 2 I
78 77 sselda I V F X G X k supp 0 F supp 0 G supp 0 x I F x G x 2 k I
79 78 62 syldan I V F X G X k supp 0 F supp 0 G supp 0 x I F x G x 2 F k G k 2 = x I F x G x 2 k
80 76 ssdifd I V F X G X supp 0 F supp 0 G supp 0 x I F x G x 2 I supp 0 x I F x G x 2
81 80 sselda I V F X G X k supp 0 F supp 0 G supp 0 x I F x G x 2 k I supp 0 x I F x G x 2
82 ssidd I V F X G X x I F x G x 2 supp 0 x I F x G x 2 supp 0
83 0cnd I V F X G X 0
84 29 82 44 83 suppssr I V F X G X k I supp 0 x I F x G x 2 x I F x G x 2 k = 0
85 81 84 syldan I V F X G X k supp 0 F supp 0 G supp 0 x I F x G x 2 x I F x G x 2 k = 0
86 79 85 eqtrd I V F X G X k supp 0 F supp 0 G supp 0 x I F x G x 2 F k G k 2 = 0
87 34 73 86 33 fsumss I V F X G X k x I F x G x 2 supp 0 F k G k 2 = k supp 0 F supp 0 G F k G k 2
88 87 adantr I V F X G X f = F g = G k x I F x G x 2 supp 0 F k G k 2 = k supp 0 F supp 0 G F k G k 2
89 20 66 88 3eqtrd I V F X G X f = F g = G fld x I f x g x 2 = k supp 0 F supp 0 G F k G k 2
90 89 fveq2d I V F X G X f = F g = G fld x I f x g x 2 = k supp 0 F supp 0 G F k G k 2
91 fvexd I V F X G X k supp 0 F supp 0 G F k G k 2 V
92 12 90 21 24 91 ovmpod I V F X G X F D G = k supp 0 F supp 0 G F k G k 2