Step |
Hyp |
Ref |
Expression |
1 |
|
elex |
|- ( X e. V -> X e. _V ) |
2 |
|
id |
|- ( u = X -> u = X ) |
3 |
2
|
sqxpeqd |
|- ( u = X -> ( u X. u ) = ( X X. X ) ) |
4 |
3
|
oveq2d |
|- ( u = X -> ( RR* ^m ( u X. u ) ) = ( RR* ^m ( X X. X ) ) ) |
5 |
|
raleq |
|- ( u = X -> ( A. z e. u ( x d y ) <_ ( ( z d x ) +e ( z d y ) ) <-> A. z e. X ( x d y ) <_ ( ( z d x ) +e ( z d y ) ) ) ) |
6 |
5
|
raleqbi1dv |
|- ( u = X -> ( A. y e. u A. z e. u ( x d y ) <_ ( ( z d x ) +e ( z d y ) ) <-> A. y e. X A. z e. X ( x d y ) <_ ( ( z d x ) +e ( z d y ) ) ) ) |
7 |
6
|
anbi2d |
|- ( u = X -> ( ( ( x d x ) = 0 /\ A. y e. u A. z e. u ( x d y ) <_ ( ( z d x ) +e ( z d y ) ) ) <-> ( ( x d x ) = 0 /\ A. y e. X A. z e. X ( x d y ) <_ ( ( z d x ) +e ( z d y ) ) ) ) ) |
8 |
7
|
raleqbi1dv |
|- ( u = X -> ( A. x e. u ( ( x d x ) = 0 /\ A. y e. u A. z e. u ( x d y ) <_ ( ( z d x ) +e ( z d y ) ) ) <-> A. x e. X ( ( x d x ) = 0 /\ A. y e. X A. z e. X ( x d y ) <_ ( ( z d x ) +e ( z d y ) ) ) ) ) |
9 |
4 8
|
rabeqbidv |
|- ( u = X -> { d e. ( RR* ^m ( u X. u ) ) | A. x e. u ( ( x d x ) = 0 /\ A. y e. u A. z e. u ( x d y ) <_ ( ( z d x ) +e ( z d y ) ) ) } = { d e. ( RR* ^m ( X X. X ) ) | A. x e. X ( ( x d x ) = 0 /\ A. y e. X A. z e. X ( x d y ) <_ ( ( z d x ) +e ( z d y ) ) ) } ) |
10 |
|
df-psmet |
|- PsMet = ( u e. _V |-> { d e. ( RR* ^m ( u X. u ) ) | A. x e. u ( ( x d x ) = 0 /\ A. y e. u A. z e. u ( x d y ) <_ ( ( z d x ) +e ( z d y ) ) ) } ) |
11 |
|
ovex |
|- ( RR* ^m ( X X. X ) ) e. _V |
12 |
11
|
rabex |
|- { d e. ( RR* ^m ( X X. X ) ) | A. x e. X ( ( x d x ) = 0 /\ A. y e. X A. z e. X ( x d y ) <_ ( ( z d x ) +e ( z d y ) ) ) } e. _V |
13 |
9 10 12
|
fvmpt |
|- ( X e. _V -> ( PsMet ` X ) = { d e. ( RR* ^m ( X X. X ) ) | A. x e. X ( ( x d x ) = 0 /\ A. y e. X A. z e. X ( x d y ) <_ ( ( z d x ) +e ( z d y ) ) ) } ) |
14 |
1 13
|
syl |
|- ( X e. V -> ( PsMet ` X ) = { d e. ( RR* ^m ( X X. X ) ) | A. x e. X ( ( x d x ) = 0 /\ A. y e. X A. z e. X ( x d y ) <_ ( ( z d x ) +e ( z d y ) ) ) } ) |
15 |
14
|
eleq2d |
|- ( X e. V -> ( D e. ( PsMet ` X ) <-> D e. { d e. ( RR* ^m ( X X. X ) ) | A. x e. X ( ( x d x ) = 0 /\ A. y e. X A. z e. X ( x d y ) <_ ( ( z d x ) +e ( z d y ) ) ) } ) ) |
16 |
|
oveq |
|- ( d = D -> ( x d x ) = ( x D x ) ) |
17 |
16
|
eqeq1d |
|- ( d = D -> ( ( x d x ) = 0 <-> ( x D x ) = 0 ) ) |
18 |
|
oveq |
|- ( d = D -> ( x d y ) = ( x D 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 ) +e ( z d y ) ) = ( ( z D x ) +e ( z D y ) ) ) |
22 |
18 21
|
breq12d |
|- ( d = D -> ( ( x d y ) <_ ( ( z d x ) +e ( z d y ) ) <-> ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) |
23 |
22
|
2ralbidv |
|- ( d = D -> ( A. y e. X A. z e. X ( x d y ) <_ ( ( z d x ) +e ( z d y ) ) <-> A. y e. X A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) |
24 |
17 23
|
anbi12d |
|- ( d = D -> ( ( ( x d x ) = 0 /\ A. y e. X A. z e. X ( x d y ) <_ ( ( z d x ) +e ( z d y ) ) ) <-> ( ( x D x ) = 0 /\ A. y e. X A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) ) |
25 |
24
|
ralbidv |
|- ( d = D -> ( A. x e. X ( ( x d x ) = 0 /\ A. y e. X A. z e. X ( x d y ) <_ ( ( z d x ) +e ( z d y ) ) ) <-> A. x e. X ( ( x D x ) = 0 /\ A. y e. X A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) ) |
26 |
25
|
elrab |
|- ( D e. { d e. ( RR* ^m ( X X. X ) ) | A. x e. X ( ( x d x ) = 0 /\ A. y e. X A. z e. X ( x d y ) <_ ( ( z d x ) +e ( z d y ) ) ) } <-> ( D e. ( RR* ^m ( X X. X ) ) /\ A. x e. X ( ( x D x ) = 0 /\ A. y e. X A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) ) |
27 |
15 26
|
bitrdi |
|- ( X e. V -> ( D e. ( PsMet ` X ) <-> ( D e. ( RR* ^m ( X X. X ) ) /\ A. x e. X ( ( x D x ) = 0 /\ A. y e. X A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) ) ) |
28 |
|
xrex |
|- RR* e. _V |
29 |
|
sqxpexg |
|- ( X e. V -> ( X X. X ) e. _V ) |
30 |
|
elmapg |
|- ( ( RR* e. _V /\ ( X X. X ) e. _V ) -> ( D e. ( RR* ^m ( X X. X ) ) <-> D : ( X X. X ) --> RR* ) ) |
31 |
28 29 30
|
sylancr |
|- ( X e. V -> ( D e. ( RR* ^m ( X X. X ) ) <-> D : ( X X. X ) --> RR* ) ) |
32 |
31
|
anbi1d |
|- ( X e. V -> ( ( D e. ( RR* ^m ( X X. X ) ) /\ A. x e. X ( ( x D x ) = 0 /\ A. y e. X A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) <-> ( D : ( X X. X ) --> RR* /\ A. x e. X ( ( x D x ) = 0 /\ A. y e. X A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) ) ) |
33 |
27 32
|
bitrd |
|- ( X e. V -> ( D e. ( PsMet ` X ) <-> ( D : ( X X. X ) --> RR* /\ A. x e. X ( ( x D x ) = 0 /\ A. y e. X A. z e. X ( x D y ) <_ ( ( z D x ) +e ( z D y ) ) ) ) ) ) |