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 D B ˙ = A D B

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 y z = a D b
3 2 3ad2ant1 D PsMet X A X B X pstoMet D = x X / ˙ , y X / ˙ z | a x b y z = a D b
4 3 oveqd D PsMet X A X B X A ˙ pstoMet D B ˙ = A ˙ x X / ˙ , y X / ˙ z | a x b y z = a D b B ˙
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 y z = a D b a A ˙ b y z = a D b
11 10 abbidv x = A ˙ z | a x b y z = a D b = z | a A ˙ b y z = a D b
12 11 unieqd x = A ˙ z | a x b y z = a D b = z | a A ˙ b y z = a D b
13 rexeq y = B ˙ b y z = a D b b B ˙ z = a D b
14 13 rexbidv y = B ˙ a A ˙ b y z = a D b a A ˙ b B ˙ z = a D b
15 14 abbidv y = B ˙ z | a A ˙ b y z = a D b = z | a A ˙ b B ˙ z = a D b
16 15 unieqd y = B ˙ z | a A ˙ b y z = a D b = z | a A ˙ b B ˙ z = a D b
17 eqid x X / ˙ , y X / ˙ z | a x b y z = a D b = x X / ˙ , y X / ˙ z | a x b y z = a D b
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 = a D b V
23 22 uniex z | a A ˙ b B ˙ z = a D b V
24 12 16 17 23 ovmpo A ˙ X / ˙ B ˙ X / ˙ A ˙ x X / ˙ , y X / ˙ z | a x b y z = a D b B ˙ = z | a A ˙ b B ˙ z = a D b
25 7 9 24 syl2anc D PsMet X A X B X A ˙ x X / ˙ , y X / ˙ z | a x b y z = a D b B ˙ = z | a A ˙ b B ˙ z = a D b
26 simpr3 D PsMet X A X B X e A ˙ f B ˙ z = e D f z = e D f
27 simpl1 D PsMet X A X B X e A ˙ f B ˙ z = e D f D PsMet X
28 simpr1 D PsMet X A X B X e A ˙ f B ˙ z = e D f 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 = e D f Rel ˙
37 relelec Rel ˙ e A ˙ A ˙ e
38 36 37 syl D PsMet X A X B X e A ˙ f B ˙ z = e D f e A ˙ A ˙ e
39 28 38 mpbid D PsMet X A X B X e A ˙ f B ˙ z = e D f A ˙ e
40 1 breqi A ˙ e A ~ Met D e
41 39 40 sylib D PsMet X A X B X e A ˙ f B ˙ z = e D f A ~ Met D e
42 simpr2 D PsMet X A X B X e A ˙ f B ˙ z = e D f 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 = e D f f B ˙ B ˙ f
45 42 44 mpbid D PsMet X A X B X e A ˙ f B ˙ z = e D f B ˙ f
46 1 breqi B ˙ f B ~ Met D f
47 45 46 sylib D PsMet X A X B X e A ˙ f B ˙ z = e D f B ~ Met D f
48 metideq D PsMet X A ~ Met D e B ~ Met D f A D B = e D f
49 27 41 47 48 syl12anc D PsMet X A X B X e A ˙ f B ˙ z = e D f A D B = e D f
50 26 49 eqtr4d D PsMet X A X B X e A ˙ f B ˙ z = e D f z = A D B
51 50 adantlr D PsMet X A X B X a A ˙ b B ˙ z = a D b e A ˙ f B ˙ z = e D f z = A D B
52 51 3anassrs D PsMet X A X B X a A ˙ b B ˙ z = a D b e A ˙ f B ˙ z = e D f z = A D B
53 oveq1 a = e a D b = e D b
54 53 eqeq2d a = e z = a D b z = e D b
55 oveq2 b = f e D b = e D f
56 55 eqeq2d b = f z = e D b z = e D f
57 54 56 cbvrex2vw a A ˙ b B ˙ z = a D b e A ˙ f B ˙ z = e D f
58 57 biimpi a A ˙ b B ˙ z = a D b e A ˙ f B ˙ z = e D f
59 58 adantl D PsMet X A X B X a A ˙ b B ˙ z = a D b e A ˙ f B ˙ z = e D f
60 52 59 r19.29vva D PsMet X A X B X a A ˙ b B ˙ z = a D b z = A D B
61 simpl1 D PsMet X A X B X z = A D B D PsMet X
62 simpl2 D PsMet X A X B X z = A D B A X
63 psmet0 D PsMet X A X A D A = 0
64 61 62 63 syl2anc D PsMet X A X B X z = A D B A D A = 0
65 relelec Rel ˙ A A ˙ A ˙ A
66 61 34 65 3syl D PsMet X A X B X z = A D B A A ˙ A ˙ A
67 1 a1i D PsMet X A X B X z = A D B ˙ = ~ Met D
68 67 breqd D PsMet X A X B X z = A D B A ˙ A A ~ Met D A
69 metidv D PsMet X A X A X A ~ Met D A A D A = 0
70 61 62 62 69 syl12anc D PsMet X A X B X z = A D B A ~ Met D A A D A = 0
71 66 68 70 3bitrd D PsMet X A X B X z = A D B A A ˙ A D A = 0
72 64 71 mpbird D PsMet X A X B X z = A D B A A ˙
73 simpl3 D PsMet X A X B X z = A D B B X
74 psmet0 D PsMet X B X B D B = 0
75 61 73 74 syl2anc D PsMet X A X B X z = A D B B D B = 0
76 relelec Rel ˙ B B ˙ B ˙ B
77 61 34 76 3syl D PsMet X A X B X z = A D B B B ˙ B ˙ B
78 67 breqd D PsMet X A X B X z = A D B B ˙ B B ~ Met D B
79 metidv D PsMet X B X B X B ~ Met D B B D B = 0
80 61 73 73 79 syl12anc D PsMet X A X B X z = A D B B ~ Met D B B D B = 0
81 77 78 80 3bitrd D PsMet X A X B X z = A D B B B ˙ B D B = 0
82 75 81 mpbird D PsMet X A X B X z = A D B B B ˙
83 simpr D PsMet X A X B X z = A D B z = A D B
84 rspceov A A ˙ B B ˙ z = A D B a A ˙ b B ˙ z = a D b
85 72 82 83 84 syl3anc D PsMet X A X B X z = A D B a A ˙ b B ˙ z = a D b
86 60 85 impbida D PsMet X A X B X a A ˙ b B ˙ z = a D b z = A D B
87 86 abbidv D PsMet X A X B X z | a A ˙ b B ˙ z = a D b = z | z = A D B
88 df-sn A D B = z | z = A D B
89 87 88 eqtr4di D PsMet X A X B X z | a A ˙ b B ˙ z = a D b = A D B
90 89 unieqd D PsMet X A X B X z | a A ˙ b B ˙ z = a D b = A D B
91 ovex A D B V
92 91 unisn A D B = A D B
93 90 92 eqtrdi D PsMet X A X B X z | a A ˙ b B ˙ z = a D b = A D B
94 4 25 93 3eqtrd D PsMet X A X B X A ˙ pstoMet D B ˙ = A D B