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∈XxDx=0∧∀y∈X∀z∈XxDy≤zDx+𝑒zDy

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∈uxdy≤zdx+𝑒zdy↔∀z∈Xxdy≤zdx+𝑒zdy
6 5 raleqbi1dv ⊢u=X→∀y∈u∀z∈uxdy≤zdx+𝑒zdy↔∀y∈X∀z∈Xxdy≤zdx+𝑒zdy
7 6 anbi2d ⊢u=X→xdx=0∧∀y∈u∀z∈uxdy≤zdx+𝑒zdy↔xdx=0∧∀y∈X∀z∈Xxdy≤zdx+𝑒zdy
8 7 raleqbi1dv ⊢u=X→∀x∈uxdx=0∧∀y∈u∀z∈uxdy≤zdx+𝑒zdy↔∀x∈Xxdx=0∧∀y∈X∀z∈Xxdy≤zdx+𝑒zdy
9 4 8 rabeqbidv ⊢u=X→d∈ℝ*u×u|∀x∈uxdx=0∧∀y∈u∀z∈uxdy≤zdx+𝑒zdy=d∈ℝ*X×X|∀x∈Xxdx=0∧∀y∈X∀z∈Xxdy≤zdx+𝑒zdy
10 df-psmet ⊢PsMet=u∈V⟼d∈ℝ*u×u|∀x∈uxdx=0∧∀y∈u∀z∈uxdy≤zdx+𝑒zdy
11 ovex ⊢ℝ*X×X∈V
12 11 rabex ⊢d∈ℝ*X×X|∀x∈Xxdx=0∧∀y∈X∀z∈Xxdy≤zdx+𝑒zdy∈V
13 9 10 12 fvmpt ⊢X∈V→PsMet⁡X=d∈ℝ*X×X|∀x∈Xxdx=0∧∀y∈X∀z∈Xxdy≤zdx+𝑒zdy
14 1 13 syl ⊢X∈V→PsMet⁡X=d∈ℝ*X×X|∀x∈Xxdx=0∧∀y∈X∀z∈Xxdy≤zdx+𝑒zdy
15 14 eleq2d ⊢X∈V→D∈PsMet⁡X↔D∈d∈ℝ*X×X|∀x∈Xxdx=0∧∀y∈X∀z∈Xxdy≤zdx+𝑒zdy
16 oveq ⊢d=D→xdx=xDx
17 16 eqeq1d ⊢d=D→xdx=0↔xDx=0
18 oveq ⊢d=D→xdy=xDy
19 oveq ⊢d=D→zdx=zDx
20 oveq ⊢d=D→zdy=zDy
21 19 20 oveq12d ⊢d=D→zdx+𝑒zdy=zDx+𝑒zDy
22 18 21 breq12d ⊢d=D→xdy≤zdx+𝑒zdy↔xDy≤zDx+𝑒zDy
23 22 2ralbidv ⊢d=D→∀y∈X∀z∈Xxdy≤zdx+𝑒zdy↔∀y∈X∀z∈XxDy≤zDx+𝑒zDy
24 17 23 anbi12d ⊢d=D→xdx=0∧∀y∈X∀z∈Xxdy≤zdx+𝑒zdy↔xDx=0∧∀y∈X∀z∈XxDy≤zDx+𝑒zDy
25 24 ralbidv ⊢d=D→∀x∈Xxdx=0∧∀y∈X∀z∈Xxdy≤zdx+𝑒zdy↔∀x∈XxDx=0∧∀y∈X∀z∈XxDy≤zDx+𝑒zDy
26 25 elrab ⊢D∈d∈ℝ*X×X|∀x∈Xxdx=0∧∀y∈X∀z∈Xxdy≤zdx+𝑒zdy↔D∈ℝ*X×X∧∀x∈XxDx=0∧∀y∈X∀z∈XxDy≤zDx+𝑒zDy
27 15 26 bitrdi ⊢X∈V→D∈PsMet⁡X↔D∈ℝ*X×X∧∀x∈XxDx=0∧∀y∈X∀z∈XxDy≤zDx+𝑒zDy
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∈XxDx=0∧∀y∈X∀z∈XxDy≤zDx+𝑒zDy↔D:X×X⟶ℝ*∧∀x∈XxDx=0∧∀y∈X∀z∈XxDy≤zDx+𝑒zDy
33 27 32 bitrd ⊢X∈V→D∈PsMet⁡X↔D:X×X⟶ℝ*∧∀x∈XxDx=0∧∀y∈X∀z∈XxDy≤zDx+𝑒zDy