Step |
Hyp |
Ref |
Expression |
1 |
|
elfvex |
|- ( D e. ( PsMet ` X ) -> X e. _V ) |
2 |
|
ispsmet |
|- ( X e. _V -> ( D e. ( PsMet ` X ) <-> ( D : ( X X. X ) --> RR* /\ A. a e. X ( ( a D a ) = 0 /\ A. b e. X A. c e. X ( a D b ) <_ ( ( c D a ) +e ( c D b ) ) ) ) ) ) |
3 |
1 2
|
syl |
|- ( D e. ( PsMet ` X ) -> ( D e. ( PsMet ` X ) <-> ( D : ( X X. X ) --> RR* /\ A. a e. X ( ( a D a ) = 0 /\ A. b e. X A. c e. X ( a D b ) <_ ( ( c D a ) +e ( c D b ) ) ) ) ) ) |
4 |
3
|
ibi |
|- ( D e. ( PsMet ` X ) -> ( D : ( X X. X ) --> RR* /\ A. a e. X ( ( a D a ) = 0 /\ A. b e. X A. c e. X ( a D b ) <_ ( ( c D a ) +e ( c D b ) ) ) ) ) |
5 |
4
|
simprd |
|- ( D e. ( PsMet ` X ) -> A. a e. X ( ( a D a ) = 0 /\ A. b e. X A. c e. X ( a D b ) <_ ( ( c D a ) +e ( c D b ) ) ) ) |
6 |
5
|
r19.21bi |
|- ( ( D e. ( PsMet ` X ) /\ a e. X ) -> ( ( a D a ) = 0 /\ A. b e. X A. c e. X ( a D b ) <_ ( ( c D a ) +e ( c D b ) ) ) ) |
7 |
6
|
simpld |
|- ( ( D e. ( PsMet ` X ) /\ a e. X ) -> ( a D a ) = 0 ) |
8 |
7
|
ralrimiva |
|- ( D e. ( PsMet ` X ) -> A. a e. X ( a D a ) = 0 ) |
9 |
|
id |
|- ( a = A -> a = A ) |
10 |
9 9
|
oveq12d |
|- ( a = A -> ( a D a ) = ( A D A ) ) |
11 |
10
|
eqeq1d |
|- ( a = A -> ( ( a D a ) = 0 <-> ( A D A ) = 0 ) ) |
12 |
11
|
rspcv |
|- ( A e. X -> ( A. a e. X ( a D a ) = 0 -> ( A D A ) = 0 ) ) |
13 |
8 12
|
mpan9 |
|- ( ( D e. ( PsMet ` X ) /\ A e. X ) -> ( A D A ) = 0 ) |