Metamath Proof Explorer

Theorem pstmfval

Description: Function value of the metric induced by a pseudometric D (Contributed by Thierry Arnoux, 11-Feb-2018)

Ref Expression
Hypothesis pstmval.1 ⊢∼˙=~Met⁡D
Assertion pstmfval ⊢D∈PsMet⁡X∧A∈X∧B∈X→A∼˙pstoMet⁡DB∼˙=ADB

Proof

Step Hyp Ref Expression
1 pstmval.1 ⊢∼˙=~Met⁡D
2 1 pstmval ⊢D∈PsMet⁡X→pstoMet⁡D=x∈X/∼˙,y∈X/∼˙⟼⋃z|∃a∈x∃b∈yz=aDb
3 2 3ad2ant1 ⊢D∈PsMet⁡X∧A∈X∧B∈X→pstoMet⁡D=x∈X/∼˙,y∈X/∼˙⟼⋃z|∃a∈x∃b∈yz=aDb
4 3 oveqd ⊢D∈PsMet⁡X∧A∈X∧B∈X→A∼˙pstoMet⁡DB∼˙=A∼˙x∈X/∼˙,y∈X/∼˙⟼⋃z|∃a∈x∃b∈yz=aDbB∼˙
5 1 fvexi ⊢∼˙∈V
6 5 ecelqsi ⊢A∈X→A∼˙∈X/∼˙
7 6 3ad2ant2 ⊢D∈PsMet⁡X∧A∈X∧B∈X→A∼˙∈X/∼˙
8 5 ecelqsi ⊢B∈X→B∼˙∈X/∼˙
9 8 3ad2ant3 ⊢D∈PsMet⁡X∧A∈X∧B∈X→B∼˙∈X/∼˙
10 rexeq ⊢x=A∼˙→∃a∈x∃b∈yz=aDb↔∃a∈A∼˙∃b∈yz=aDb
11 10 abbidv ⊢x=A∼˙→z|∃a∈x∃b∈yz=aDb=z|∃a∈A∼˙∃b∈yz=aDb
12 11 unieqd ⊢x=A∼˙→⋃z|∃a∈x∃b∈yz=aDb=⋃z|∃a∈A∼˙∃b∈yz=aDb
13 rexeq ⊢y=B∼˙→∃b∈yz=aDb↔∃b∈B∼˙z=aDb
14 13 rexbidv ⊢y=B∼˙→∃a∈A∼˙∃b∈yz=aDb↔∃a∈A∼˙∃b∈B∼˙z=aDb
15 14 abbidv ⊢y=B∼˙→z|∃a∈A∼˙∃b∈yz=aDb=z|∃a∈A∼˙∃b∈B∼˙z=aDb
16 15 unieqd ⊢y=B∼˙→⋃z|∃a∈A∼˙∃b∈yz=aDb=⋃z|∃a∈A∼˙∃b∈B∼˙z=aDb
17 eqid ⊢x∈X/∼˙,y∈X/∼˙⟼⋃z|∃a∈x∃b∈yz=aDb=x∈X/∼˙,y∈X/∼˙⟼⋃z|∃a∈x∃b∈yz=aDb
18 ecexg ⊢∼˙∈V→A∼˙∈V
19 5 18 ax-mp ⊢A∼˙∈V
20 ecexg ⊢∼˙∈V→B∼˙∈V
21 5 20 ax-mp ⊢B∼˙∈V
22 19 21 ab2rexex ⊢z|∃a∈A∼˙∃b∈B∼˙z=aDb∈V
23 22 uniex ⊢⋃z|∃a∈A∼˙∃b∈B∼˙z=aDb∈V
24 12 16 17 23 ovmpo ⊢A∼˙∈X/∼˙∧B∼˙∈X/∼˙→A∼˙x∈X/∼˙,y∈X/∼˙⟼⋃z|∃a∈x∃b∈yz=aDbB∼˙=⋃z|∃a∈A∼˙∃b∈B∼˙z=aDb
25 7 9 24 syl2anc ⊢D∈PsMet⁡X∧A∈X∧B∈X→A∼˙x∈X/∼˙,y∈X/∼˙⟼⋃z|∃a∈x∃b∈yz=aDbB∼˙=⋃z|∃a∈A∼˙∃b∈B∼˙z=aDb
26 simpr3 ⊢D∈PsMet⁡X∧A∈X∧B∈X∧e∈A∼˙∧f∈B∼˙∧z=eDf→z=eDf
27 simpl1 ⊢D∈PsMet⁡X∧A∈X∧B∈X∧e∈A∼˙∧f∈B∼˙∧z=eDf→D∈PsMet⁡X
28 simpr1 ⊢D∈PsMet⁡X∧A∈X∧B∈X∧e∈A∼˙∧f∈B∼˙∧z=eDf→e∈A∼˙
29 metidss ⊢D∈PsMet⁡X→~Met⁡D⊆X×X
30 1 29 eqsstrid ⊢D∈PsMet⁡X→∼˙⊆X×X
31 xpss ⊢X×X⊆V×V
32 30 31 sstrdi ⊢D∈PsMet⁡X→∼˙⊆V×V
33 df-rel ⊢Rel⁡∼˙↔∼˙⊆V×V
34 32 33 sylibr ⊢D∈PsMet⁡X→Rel⁡∼˙
35 34 3ad2ant1 ⊢D∈PsMet⁡X∧A∈X∧B∈X→Rel⁡∼˙
36 35 adantr ⊢D∈PsMet⁡X∧A∈X∧B∈X∧e∈A∼˙∧f∈B∼˙∧z=eDf→Rel⁡∼˙
37 relelec ⊢Rel⁡∼˙→e∈A∼˙↔A∼˙e
38 36 37 syl ⊢D∈PsMet⁡X∧A∈X∧B∈X∧e∈A∼˙∧f∈B∼˙∧z=eDf→e∈A∼˙↔A∼˙e
39 28 38 mpbid ⊢D∈PsMet⁡X∧A∈X∧B∈X∧e∈A∼˙∧f∈B∼˙∧z=eDf→A∼˙e
40 1 breqi ⊢A∼˙e↔A~Met⁡De
41 39 40 sylib ⊢D∈PsMet⁡X∧A∈X∧B∈X∧e∈A∼˙∧f∈B∼˙∧z=eDf→A~Met⁡De
42 simpr2 ⊢D∈PsMet⁡X∧A∈X∧B∈X∧e∈A∼˙∧f∈B∼˙∧z=eDf→f∈B∼˙
43 relelec ⊢Rel⁡∼˙→f∈B∼˙↔B∼˙f
44 36 43 syl ⊢D∈PsMet⁡X∧A∈X∧B∈X∧e∈A∼˙∧f∈B∼˙∧z=eDf→f∈B∼˙↔B∼˙f
45 42 44 mpbid ⊢D∈PsMet⁡X∧A∈X∧B∈X∧e∈A∼˙∧f∈B∼˙∧z=eDf→B∼˙f
46 1 breqi ⊢B∼˙f↔B~Met⁡Df
47 45 46 sylib ⊢D∈PsMet⁡X∧A∈X∧B∈X∧e∈A∼˙∧f∈B∼˙∧z=eDf→B~Met⁡Df
48 metideq ⊢D∈PsMet⁡X∧A~Met⁡De∧B~Met⁡Df→ADB=eDf
49 27 41 47 48 syl12anc ⊢D∈PsMet⁡X∧A∈X∧B∈X∧e∈A∼˙∧f∈B∼˙∧z=eDf→ADB=eDf
50 26 49 eqtr4d ⊢D∈PsMet⁡X∧A∈X∧B∈X∧e∈A∼˙∧f∈B∼˙∧z=eDf→z=ADB
51 50 adantlr ⊢D∈PsMet⁡X∧A∈X∧B∈X∧∃a∈A∼˙∃b∈B∼˙z=aDb∧e∈A∼˙∧f∈B∼˙∧z=eDf→z=ADB
52 51 3anassrs ⊢D∈PsMet⁡X∧A∈X∧B∈X∧∃a∈A∼˙∃b∈B∼˙z=aDb∧e∈A∼˙∧f∈B∼˙∧z=eDf→z=ADB
53 oveq1 ⊢a=e→aDb=eDb
54 53 eqeq2d ⊢a=e→z=aDb↔z=eDb
55 oveq2 ⊢b=f→eDb=eDf
56 55 eqeq2d ⊢b=f→z=eDb↔z=eDf
57 54 56 cbvrex2vw ⊢∃a∈A∼˙∃b∈B∼˙z=aDb↔∃e∈A∼˙∃f∈B∼˙z=eDf
58 57 biimpi ⊢∃a∈A∼˙∃b∈B∼˙z=aDb→∃e∈A∼˙∃f∈B∼˙z=eDf
59 58 adantl ⊢D∈PsMet⁡X∧A∈X∧B∈X∧∃a∈A∼˙∃b∈B∼˙z=aDb→∃e∈A∼˙∃f∈B∼˙z=eDf
60 52 59 r19.29vva ⊢D∈PsMet⁡X∧A∈X∧B∈X∧∃a∈A∼˙∃b∈B∼˙z=aDb→z=ADB
61 simpl1 ⊢D∈PsMet⁡X∧A∈X∧B∈X∧z=ADB→D∈PsMet⁡X
62 simpl2 ⊢D∈PsMet⁡X∧A∈X∧B∈X∧z=ADB→A∈X
63 psmet0 ⊢D∈PsMet⁡X∧A∈X→ADA=0
64 61 62 63 syl2anc ⊢D∈PsMet⁡X∧A∈X∧B∈X∧z=ADB→ADA=0
65 relelec ⊢Rel⁡∼˙→A∈A∼˙↔A∼˙A
66 61 34 65 3syl ⊢D∈PsMet⁡X∧A∈X∧B∈X∧z=ADB→A∈A∼˙↔A∼˙A
67 1 a1i ⊢D∈PsMet⁡X∧A∈X∧B∈X∧z=ADB→∼˙=~Met⁡D
68 67 breqd ⊢D∈PsMet⁡X∧A∈X∧B∈X∧z=ADB→A∼˙A↔A~Met⁡DA
69 metidv ⊢D∈PsMet⁡X∧A∈X∧A∈X→A~Met⁡DA↔ADA=0
70 61 62 62 69 syl12anc ⊢D∈PsMet⁡X∧A∈X∧B∈X∧z=ADB→A~Met⁡DA↔ADA=0
71 66 68 70 3bitrd ⊢D∈PsMet⁡X∧A∈X∧B∈X∧z=ADB→A∈A∼˙↔ADA=0
72 64 71 mpbird ⊢D∈PsMet⁡X∧A∈X∧B∈X∧z=ADB→A∈A∼˙
73 simpl3 ⊢D∈PsMet⁡X∧A∈X∧B∈X∧z=ADB→B∈X
74 psmet0 ⊢D∈PsMet⁡X∧B∈X→BDB=0
75 61 73 74 syl2anc ⊢D∈PsMet⁡X∧A∈X∧B∈X∧z=ADB→BDB=0
76 relelec ⊢Rel⁡∼˙→B∈B∼˙↔B∼˙B
77 61 34 76 3syl ⊢D∈PsMet⁡X∧A∈X∧B∈X∧z=ADB→B∈B∼˙↔B∼˙B
78 67 breqd ⊢D∈PsMet⁡X∧A∈X∧B∈X∧z=ADB→B∼˙B↔B~Met⁡DB
79 metidv ⊢D∈PsMet⁡X∧B∈X∧B∈X→B~Met⁡DB↔BDB=0
80 61 73 73 79 syl12anc ⊢D∈PsMet⁡X∧A∈X∧B∈X∧z=ADB→B~Met⁡DB↔BDB=0
81 77 78 80 3bitrd ⊢D∈PsMet⁡X∧A∈X∧B∈X∧z=ADB→B∈B∼˙↔BDB=0
82 75 81 mpbird ⊢D∈PsMet⁡X∧A∈X∧B∈X∧z=ADB→B∈B∼˙
83 simpr ⊢D∈PsMet⁡X∧A∈X∧B∈X∧z=ADB→z=ADB
84 rspceov ⊢A∈A∼˙∧B∈B∼˙∧z=ADB→∃a∈A∼˙∃b∈B∼˙z=aDb
85 72 82 83 84 syl3anc ⊢D∈PsMet⁡X∧A∈X∧B∈X∧z=ADB→∃a∈A∼˙∃b∈B∼˙z=aDb
86 60 85 impbida ⊢D∈PsMet⁡X∧A∈X∧B∈X→∃a∈A∼˙∃b∈B∼˙z=aDb↔z=ADB
87 86 abbidv ⊢D∈PsMet⁡X∧A∈X∧B∈X→z|∃a∈A∼˙∃b∈B∼˙z=aDb=z|z=ADB
88 df-sn ⊢ADB=z|z=ADB
89 87 88 eqtr4di ⊢D∈PsMet⁡X∧A∈X∧B∈X→z|∃a∈A∼˙∃b∈B∼˙z=aDb=ADB
90 89 unieqd ⊢D∈PsMet⁡X∧A∈X∧B∈X→⋃z|∃a∈A∼˙∃b∈B∼˙z=aDb=⋃ADB
91 ovex ⊢ADB∈V
92 91 unisn ⊢⋃ADB=ADB
93 90 92 eqtrdi ⊢D∈PsMet⁡X∧A∈X∧B∈X→⋃z|∃a∈A∼˙∃b∈B∼˙z=aDb=ADB
94 4 25 93 3eqtrd ⊢D∈PsMet⁡X∧A∈X∧B∈X→A∼˙pstoMet⁡DB∼˙=ADB