Metamath Proof Explorer


Theorem isxmet

Description: Express the predicate " D is an extended metric." (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Assertion isxmet 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-xmet ∞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 xrex * 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