Metamath Proof Explorer


Theorem ismet

Description: Express the predicate " D is a metric." (Contributed by NM, 25-Aug-2006) (Revised by Mario Carneiro, 14-Aug-2015)

Ref Expression
Assertion ismet X A D Met X D : X × X x X y X x D y = 0 x = y z X x D y z D x + z D y

Proof

Step Hyp Ref Expression
1 elex X A X V
2 xpeq12 t = X t = X t × t = X × X
3 2 anidms t = X t × t = X × X
4 3 oveq2d t = X t × t = X × X
5 raleq t = X z t x d y z d x + z d y z X x d y z d x + z d y
6 5 anbi2d t = X x d y = 0 x = y z t x d y z d x + z d y x d y = 0 x = y z X x d y z d x + z d y
7 6 raleqbi1dv t = X y t x d y = 0 x = y z t x d y z d x + z d y y X x d y = 0 x = y z X x d y z d x + z d y
8 7 raleqbi1dv t = X x t y t x d y = 0 x = y z t x d y z d x + z d y x X y X x d y = 0 x = y z X x d y z d x + z d y
9 4 8 rabeqbidv t = X d t × t | x t y t x d y = 0 x = y z t x d y z d x + z d y = d X × X | x X y X x d y = 0 x = y z X x d y z d x + z d y
10 df-met Met = t V d t × t | x t y t x d y = 0 x = y z t x d y z d x + z d y
11 ovex X × X V
12 11 rabex d X × X | x X y X x d y = 0 x = y z X x d y z d x + z d y V
13 9 10 12 fvmpt X V Met X = d X × X | x X y X x d y = 0 x = y z X x d y z d x + z d y
14 1 13 syl X A Met X = d X × X | x X y X x d y = 0 x = y z X x d y z d x + z d y
15 14 eleq2d X A D Met X D d X × X | x X y X x d y = 0 x = y z X x d y z d x + z d y
16 oveq d = D x d y = x D y
17 16 eqeq1d d = D x d y = 0 x D y = 0
18 17 bibi1d d = D x d y = 0 x = y x D y = 0 x = y
19 oveq d = D z d x = z D x
20 oveq d = D z d y = z D y
21 19 20 oveq12d d = D z d x + z d y = z D x + z D y
22 16 21 breq12d d = D x d y z d x + z d y x D y z D x + z D y
23 22 ralbidv d = D z X x d y z d x + z d y z X x D y z D x + z D y
24 18 23 anbi12d d = D x d y = 0 x = y z X x d y z d x + z d y x D y = 0 x = y z X x D y z D x + z D y
25 24 2ralbidv d = D x X y X x d y = 0 x = y z X x d y z d x + z d y x X y X x D y = 0 x = y z X x D y z D x + z D y
26 25 elrab D d X × X | x X y X x d y = 0 x = y z X x d y z d x + z d y D X × X x X y X x D y = 0 x = y z X x D y z D x + z D y
27 15 26 bitrdi X A D Met X D X × X x X y X x D y = 0 x = y z X x D y z D x + z D y
28 reex V
29 sqxpexg X A X × X V
30 elmapg V X × X V D X × X D : X × X
31 28 29 30 sylancr X A D X × X D : X × X
32 31 anbi1d X A D X × X x X y X x D y = 0 x = y z X x D y z D x + z D y D : X × X x X y X x D y = 0 x = y z X x D y z D x + z D y
33 27 32 bitrd X A D Met X D : X × X x X y X x D y = 0 x = y z X x D y z D x + z D y