Metamath Proof Explorer


Theorem ispsmet

Description: Express the predicate " D is a pseudometric." (Contributed by Thierry Arnoux, 7-Feb-2018)

Ref Expression
Assertion ispsmet X V D PsMet X D : X × X * x X x D x = 0 y X z X x D y z D x + 𝑒 z D y

Proof

Step Hyp Ref Expression
1 elex X V X V
2 id u = X u = X
3 2 sqxpeqd u = X u × u = X × X
4 3 oveq2d u = X * u × u = * X × X
5 raleq u = X z u x d y z d x + 𝑒 z d y z X x d y z d x + 𝑒 z d y
6 5 raleqbi1dv u = X y u z u x d y z d x + 𝑒 z d y y X z X x d y z d x + 𝑒 z d y
7 6 anbi2d u = X x d x = 0 y u z u x d y z d x + 𝑒 z d y x d x = 0 y X z X x d y z d x + 𝑒 z d y
8 7 raleqbi1dv u = X x u x d x = 0 y u z u x d y z d x + 𝑒 z d y x X x d x = 0 y X z X x d y z d x + 𝑒 z d y
9 4 8 rabeqbidv u = X d * u × u | x u x d x = 0 y u z u x d y z d x + 𝑒 z d y = d * X × X | x X x d x = 0 y X z X x d y z d x + 𝑒 z d y
10 df-psmet PsMet = u V d * u × u | x u x d x = 0 y u z u x d y z d x + 𝑒 z d y
11 ovex * X × X V
12 11 rabex d * X × X | x X x d x = 0 y X z X x d y z d x + 𝑒 z d y V
13 9 10 12 fvmpt X V PsMet X = d * X × X | x X x d x = 0 y X z X x d y z d x + 𝑒 z d y
14 1 13 syl X V PsMet X = d * X × X | x X x d x = 0 y X z X x d y z d x + 𝑒 z d y
15 14 eleq2d X V D PsMet X D d * X × X | x X x d x = 0 y X z X x d y z d x + 𝑒 z d y
16 oveq d = D x d x = x D x
17 16 eqeq1d d = D x d x = 0 x D x = 0
18 oveq d = D x d y = x D 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 18 21 breq12d d = D x d y z d x + 𝑒 z d y x D y z D x + 𝑒 z D y
23 22 2ralbidv d = D y X z X x d y z d x + 𝑒 z d y y X z X x D y z D x + 𝑒 z D y
24 17 23 anbi12d d = D x d x = 0 y X z X x d y z d x + 𝑒 z d y x D x = 0 y X z X x D y z D x + 𝑒 z D y
25 24 ralbidv d = D x X x d x = 0 y X z X x d y z d x + 𝑒 z d y x X x D x = 0 y X z X x D y z D x + 𝑒 z D y
26 25 elrab D d * X × X | x X x d x = 0 y X z X x d y z d x + 𝑒 z d y D * X × X x X x D x = 0 y X z X x D y z D x + 𝑒 z D y
27 15 26 bitrdi X V D PsMet X D * X × X x X x D x = 0 y X z X x D y z D x + 𝑒 z D y
28 xrex * V
29 sqxpexg X V X × X V
30 elmapg * V X × X V D * X × X D : X × X *
31 28 29 30 sylancr X V D * X × X D : X × X *
32 31 anbi1d X V D * X × X x X x D x = 0 y X z X x D y z D x + 𝑒 z D y D : X × X * x X x D x = 0 y X z X x D y z D x + 𝑒 z D y
33 27 32 bitrd X V D PsMet X D : X × X * x X x D x = 0 y X z X x D y z D x + 𝑒 z D y