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 e. ( PsMet ` X ) /\ A e. X /\ B e. X ) -> ( [ A ] .~ ( pstoMet ` D ) [ B ] .~ ) = ( A D B ) )

Proof

Step Hyp Ref Expression
1 pstmval.1 
 |-  .~ = ( ~Met ` D )
2 1 pstmval 
 |-  ( D e. ( PsMet ` X ) -> ( pstoMet ` D ) = ( x e. ( X /. .~ ) , y e. ( X /. .~ ) |-> U. { z | E. a e. x E. b e. y z = ( a D b ) } ) )
3 2 3ad2ant1 
 |-  ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) -> ( pstoMet ` D ) = ( x e. ( X /. .~ ) , y e. ( X /. .~ ) |-> U. { z | E. a e. x E. b e. y z = ( a D b ) } ) )
4 3 oveqd 
 |-  ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) -> ( [ A ] .~ ( pstoMet ` D ) [ B ] .~ ) = ( [ A ] .~ ( x e. ( X /. .~ ) , y e. ( X /. .~ ) |-> U. { z | E. a e. x E. b e. y z = ( a D b ) } ) [ B ] .~ ) )
5 1 fvexi 
 |-  .~ e. _V
6 5 ecelqsi 
 |-  ( A e. X -> [ A ] .~ e. ( X /. .~ ) )
7 6 3ad2ant2 
 |-  ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) -> [ A ] .~ e. ( X /. .~ ) )
8 5 ecelqsi 
 |-  ( B e. X -> [ B ] .~ e. ( X /. .~ ) )
9 8 3ad2ant3 
 |-  ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) -> [ B ] .~ e. ( X /. .~ ) )
10 rexeq 
 |-  ( x = [ A ] .~ -> ( E. a e. x E. b e. y z = ( a D b ) <-> E. a e. [ A ] .~ E. b e. y z = ( a D b ) ) )
11 10 abbidv 
 |-  ( x = [ A ] .~ -> { z | E. a e. x E. b e. y z = ( a D b ) } = { z | E. a e. [ A ] .~ E. b e. y z = ( a D b ) } )
12 11 unieqd 
 |-  ( x = [ A ] .~ -> U. { z | E. a e. x E. b e. y z = ( a D b ) } = U. { z | E. a e. [ A ] .~ E. b e. y z = ( a D b ) } )
13 rexeq 
 |-  ( y = [ B ] .~ -> ( E. b e. y z = ( a D b ) <-> E. b e. [ B ] .~ z = ( a D b ) ) )
14 13 rexbidv 
 |-  ( y = [ B ] .~ -> ( E. a e. [ A ] .~ E. b e. y z = ( a D b ) <-> E. a e. [ A ] .~ E. b e. [ B ] .~ z = ( a D b ) ) )
15 14 abbidv 
 |-  ( y = [ B ] .~ -> { z | E. a e. [ A ] .~ E. b e. y z = ( a D b ) } = { z | E. a e. [ A ] .~ E. b e. [ B ] .~ z = ( a D b ) } )
16 15 unieqd 
 |-  ( y = [ B ] .~ -> U. { z | E. a e. [ A ] .~ E. b e. y z = ( a D b ) } = U. { z | E. a e. [ A ] .~ E. b e. [ B ] .~ z = ( a D b ) } )
17 eqid 
 |-  ( x e. ( X /. .~ ) , y e. ( X /. .~ ) |-> U. { z | E. a e. x E. b e. y z = ( a D b ) } ) = ( x e. ( X /. .~ ) , y e. ( X /. .~ ) |-> U. { z | E. a e. x E. b e. y z = ( a D b ) } )
18 ecexg 
 |-  ( .~ e. _V -> [ A ] .~ e. _V )
19 5 18 ax-mp 
 |-  [ A ] .~ e. _V
20 ecexg 
 |-  ( .~ e. _V -> [ B ] .~ e. _V )
21 5 20 ax-mp 
 |-  [ B ] .~ e. _V
22 19 21 ab2rexex 
 |-  { z | E. a e. [ A ] .~ E. b e. [ B ] .~ z = ( a D b ) } e. _V
23 22 uniex 
 |-  U. { z | E. a e. [ A ] .~ E. b e. [ B ] .~ z = ( a D b ) } e. _V
24 12 16 17 23 ovmpo 
 |-  ( ( [ A ] .~ e. ( X /. .~ ) /\ [ B ] .~ e. ( X /. .~ ) ) -> ( [ A ] .~ ( x e. ( X /. .~ ) , y e. ( X /. .~ ) |-> U. { z | E. a e. x E. b e. y z = ( a D b ) } ) [ B ] .~ ) = U. { z | E. a e. [ A ] .~ E. b e. [ B ] .~ z = ( a D b ) } )
25 7 9 24 syl2anc 
 |-  ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) -> ( [ A ] .~ ( x e. ( X /. .~ ) , y e. ( X /. .~ ) |-> U. { z | E. a e. x E. b e. y z = ( a D b ) } ) [ B ] .~ ) = U. { z | E. a e. [ A ] .~ E. b e. [ B ] .~ z = ( a D b ) } )
26 simpr3 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) /\ ( e e. [ A ] .~ /\ f e. [ B ] .~ /\ z = ( e D f ) ) ) -> z = ( e D f ) )
27 simpl1 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) /\ ( e e. [ A ] .~ /\ f e. [ B ] .~ /\ z = ( e D f ) ) ) -> D e. ( PsMet ` X ) )
28 simpr1 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) /\ ( e e. [ A ] .~ /\ f e. [ B ] .~ /\ z = ( e D f ) ) ) -> e e. [ A ] .~ )
29 metidss 
 |-  ( D e. ( PsMet ` X ) -> ( ~Met ` D ) C_ ( X X. X ) )
30 1 29 eqsstrid 
 |-  ( D e. ( PsMet ` X ) -> .~ C_ ( X X. X ) )
31 xpss 
 |-  ( X X. X ) C_ ( _V X. _V )
32 30 31 sstrdi 
 |-  ( D e. ( PsMet ` X ) -> .~ C_ ( _V X. _V ) )
33 df-rel 
 |-  ( Rel .~ <-> .~ C_ ( _V X. _V ) )
34 32 33 sylibr 
 |-  ( D e. ( PsMet ` X ) -> Rel .~ )
35 34 3ad2ant1 
 |-  ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) -> Rel .~ )
36 35 adantr 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) /\ ( e e. [ A ] .~ /\ f e. [ B ] .~ /\ z = ( e D f ) ) ) -> Rel .~ )
37 relelec 
 |-  ( Rel .~ -> ( e e. [ A ] .~ <-> A .~ e ) )
38 36 37 syl 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) /\ ( e e. [ A ] .~ /\ f e. [ B ] .~ /\ z = ( e D f ) ) ) -> ( e e. [ A ] .~ <-> A .~ e ) )
39 28 38 mpbid 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) /\ ( e e. [ A ] .~ /\ f e. [ B ] .~ /\ z = ( e D f ) ) ) -> A .~ e )
40 1 breqi 
 |-  ( A .~ e <-> A ( ~Met ` D ) e )
41 39 40 sylib 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) /\ ( e e. [ A ] .~ /\ f e. [ B ] .~ /\ z = ( e D f ) ) ) -> A ( ~Met ` D ) e )
42 simpr2 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) /\ ( e e. [ A ] .~ /\ f e. [ B ] .~ /\ z = ( e D f ) ) ) -> f e. [ B ] .~ )
43 relelec 
 |-  ( Rel .~ -> ( f e. [ B ] .~ <-> B .~ f ) )
44 36 43 syl 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) /\ ( e e. [ A ] .~ /\ f e. [ B ] .~ /\ z = ( e D f ) ) ) -> ( f e. [ B ] .~ <-> B .~ f ) )
45 42 44 mpbid 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) /\ ( e e. [ A ] .~ /\ f e. [ B ] .~ /\ z = ( e D f ) ) ) -> B .~ f )
46 1 breqi 
 |-  ( B .~ f <-> B ( ~Met ` D ) f )
47 45 46 sylib 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) /\ ( e e. [ A ] .~ /\ f e. [ B ] .~ /\ z = ( e D f ) ) ) -> B ( ~Met ` D ) f )
48 metideq 
 |-  ( ( D e. ( PsMet ` X ) /\ ( A ( ~Met ` D ) e /\ B ( ~Met ` D ) f ) ) -> ( A D B ) = ( e D f ) )
49 27 41 47 48 syl12anc 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) /\ ( e e. [ A ] .~ /\ f e. [ B ] .~ /\ z = ( e D f ) ) ) -> ( A D B ) = ( e D f ) )
50 26 49 eqtr4d 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) /\ ( e e. [ A ] .~ /\ f e. [ B ] .~ /\ z = ( e D f ) ) ) -> z = ( A D B ) )
51 50 adantlr 
 |-  ( ( ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) /\ E. a e. [ A ] .~ E. b e. [ B ] .~ z = ( a D b ) ) /\ ( e e. [ A ] .~ /\ f e. [ B ] .~ /\ z = ( e D f ) ) ) -> z = ( A D B ) )
52 51 3anassrs 
 |-  ( ( ( ( ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) /\ E. a e. [ A ] .~ E. b e. [ B ] .~ z = ( a D b ) ) /\ e e. [ A ] .~ ) /\ f e. [ 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 
 |-  ( E. a e. [ A ] .~ E. b e. [ B ] .~ z = ( a D b ) <-> E. e e. [ A ] .~ E. f e. [ B ] .~ z = ( e D f ) )
58 57 biimpi 
 |-  ( E. a e. [ A ] .~ E. b e. [ B ] .~ z = ( a D b ) -> E. e e. [ A ] .~ E. f e. [ B ] .~ z = ( e D f ) )
59 58 adantl 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) /\ E. a e. [ A ] .~ E. b e. [ B ] .~ z = ( a D b ) ) -> E. e e. [ A ] .~ E. f e. [ B ] .~ z = ( e D f ) )
60 52 59 r19.29vva 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) /\ E. a e. [ A ] .~ E. b e. [ B ] .~ z = ( a D b ) ) -> z = ( A D B ) )
61 simpl1 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) /\ z = ( A D B ) ) -> D e. ( PsMet ` X ) )
62 simpl2 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) /\ z = ( A D B ) ) -> A e. X )
63 psmet0 
 |-  ( ( D e. ( PsMet ` X ) /\ A e. X ) -> ( A D A ) = 0 )
64 61 62 63 syl2anc 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) /\ z = ( A D B ) ) -> ( A D A ) = 0 )
65 relelec 
 |-  ( Rel .~ -> ( A e. [ A ] .~ <-> A .~ A ) )
66 61 34 65 3syl 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) /\ z = ( A D B ) ) -> ( A e. [ A ] .~ <-> A .~ A ) )
67 1 a1i 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) /\ z = ( A D B ) ) -> .~ = ( ~Met ` D ) )
68 67 breqd 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) /\ z = ( A D B ) ) -> ( A .~ A <-> A ( ~Met ` D ) A ) )
69 metidv 
 |-  ( ( D e. ( PsMet ` X ) /\ ( A e. X /\ A e. X ) ) -> ( A ( ~Met ` D ) A <-> ( A D A ) = 0 ) )
70 61 62 62 69 syl12anc 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) /\ z = ( A D B ) ) -> ( A ( ~Met ` D ) A <-> ( A D A ) = 0 ) )
71 66 68 70 3bitrd 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) /\ z = ( A D B ) ) -> ( A e. [ A ] .~ <-> ( A D A ) = 0 ) )
72 64 71 mpbird 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) /\ z = ( A D B ) ) -> A e. [ A ] .~ )
73 simpl3 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) /\ z = ( A D B ) ) -> B e. X )
74 psmet0 
 |-  ( ( D e. ( PsMet ` X ) /\ B e. X ) -> ( B D B ) = 0 )
75 61 73 74 syl2anc 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) /\ z = ( A D B ) ) -> ( B D B ) = 0 )
76 relelec 
 |-  ( Rel .~ -> ( B e. [ B ] .~ <-> B .~ B ) )
77 61 34 76 3syl 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) /\ z = ( A D B ) ) -> ( B e. [ B ] .~ <-> B .~ B ) )
78 67 breqd 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) /\ z = ( A D B ) ) -> ( B .~ B <-> B ( ~Met ` D ) B ) )
79 metidv 
 |-  ( ( D e. ( PsMet ` X ) /\ ( B e. X /\ B e. X ) ) -> ( B ( ~Met ` D ) B <-> ( B D B ) = 0 ) )
80 61 73 73 79 syl12anc 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) /\ z = ( A D B ) ) -> ( B ( ~Met ` D ) B <-> ( B D B ) = 0 ) )
81 77 78 80 3bitrd 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) /\ z = ( A D B ) ) -> ( B e. [ B ] .~ <-> ( B D B ) = 0 ) )
82 75 81 mpbird 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) /\ z = ( A D B ) ) -> B e. [ B ] .~ )
83 simpr 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) /\ z = ( A D B ) ) -> z = ( A D B ) )
84 rspceov 
 |-  ( ( A e. [ A ] .~ /\ B e. [ B ] .~ /\ z = ( A D B ) ) -> E. a e. [ A ] .~ E. b e. [ B ] .~ z = ( a D b ) )
85 72 82 83 84 syl3anc 
 |-  ( ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) /\ z = ( A D B ) ) -> E. a e. [ A ] .~ E. b e. [ B ] .~ z = ( a D b ) )
86 60 85 impbida 
 |-  ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) -> ( E. a e. [ A ] .~ E. b e. [ B ] .~ z = ( a D b ) <-> z = ( A D B ) ) )
87 86 abbidv 
 |-  ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) -> { z | E. a e. [ A ] .~ E. b e. [ 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 e. ( PsMet ` X ) /\ A e. X /\ B e. X ) -> { z | E. a e. [ A ] .~ E. b e. [ B ] .~ z = ( a D b ) } = { ( A D B ) } )
90 89 unieqd 
 |-  ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) -> U. { z | E. a e. [ A ] .~ E. b e. [ B ] .~ z = ( a D b ) } = U. { ( A D B ) } )
91 ovex 
 |-  ( A D B ) e. _V
92 91 unisn 
 |-  U. { ( A D B ) } = ( A D B )
93 90 92 eqtrdi 
 |-  ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) -> U. { z | E. a e. [ A ] .~ E. b e. [ B ] .~ z = ( a D b ) } = ( A D B ) )
94 4 25 93 3eqtrd 
 |-  ( ( D e. ( PsMet ` X ) /\ A e. X /\ B e. X ) -> ( [ A ] .~ ( pstoMet ` D ) [ B ] .~ ) = ( A D B ) )