Step |
Hyp |
Ref |
Expression |
1 |
|
xpsds.t |
|- T = ( R Xs. S ) |
2 |
|
xpsds.x |
|- X = ( Base ` R ) |
3 |
|
xpsds.y |
|- Y = ( Base ` S ) |
4 |
|
xpsds.1 |
|- ( ph -> R e. V ) |
5 |
|
xpsds.2 |
|- ( ph -> S e. W ) |
6 |
|
xpsds.p |
|- P = ( dist ` T ) |
7 |
|
xpsds.m |
|- M = ( ( dist ` R ) |` ( X X. X ) ) |
8 |
|
xpsds.n |
|- N = ( ( dist ` S ) |` ( Y X. Y ) ) |
9 |
|
xpsds.3 |
|- ( ph -> M e. ( *Met ` X ) ) |
10 |
|
xpsds.4 |
|- ( ph -> N e. ( *Met ` Y ) ) |
11 |
|
xpsds.a |
|- ( ph -> A e. X ) |
12 |
|
xpsds.b |
|- ( ph -> B e. Y ) |
13 |
|
xpsds.c |
|- ( ph -> C e. X ) |
14 |
|
xpsds.d |
|- ( ph -> D e. Y ) |
15 |
|
eqid |
|- ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) = ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) |
16 |
|
eqid |
|- ( Scalar ` R ) = ( Scalar ` R ) |
17 |
|
eqid |
|- ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) = ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) |
18 |
1 2 3 4 5 15 16 17
|
xpsval |
|- ( ph -> T = ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) "s ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) ) |
19 |
1 2 3 4 5 15 16 17
|
xpsrnbas |
|- ( ph -> ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) = ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) ) |
20 |
15
|
xpsff1o2 |
|- ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ( X X. Y ) -1-1-onto-> ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) |
21 |
|
f1ocnv |
|- ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ( X X. Y ) -1-1-onto-> ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) -> `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) -1-1-onto-> ( X X. Y ) ) |
22 |
20 21
|
mp1i |
|- ( ph -> `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) -1-1-onto-> ( X X. Y ) ) |
23 |
|
ovexd |
|- ( ph -> ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) e. _V ) |
24 |
|
eqid |
|- ( ( dist ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) |` ( ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) X. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) ) = ( ( dist ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) |` ( ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) X. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) ) |
25 |
1 2 3 4 5 6 7 8 9 10
|
xpsxmetlem |
|- ( ph -> ( dist ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) e. ( *Met ` ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) ) |
26 |
|
ssid |
|- ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) C_ ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) |
27 |
|
xmetres2 |
|- ( ( ( dist ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) e. ( *Met ` ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) /\ ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) C_ ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) -> ( ( dist ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) |` ( ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) X. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) ) e. ( *Met ` ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) ) |
28 |
25 26 27
|
sylancl |
|- ( ph -> ( ( dist ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) |` ( ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) X. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) ) e. ( *Met ` ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) ) |
29 |
|
df-ov |
|- ( A ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) B ) = ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` <. A , B >. ) |
30 |
15
|
xpsfval |
|- ( ( A e. X /\ B e. Y ) -> ( A ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) B ) = { <. (/) , A >. , <. 1o , B >. } ) |
31 |
11 12 30
|
syl2anc |
|- ( ph -> ( A ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) B ) = { <. (/) , A >. , <. 1o , B >. } ) |
32 |
29 31
|
eqtr3id |
|- ( ph -> ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` <. A , B >. ) = { <. (/) , A >. , <. 1o , B >. } ) |
33 |
11 12
|
opelxpd |
|- ( ph -> <. A , B >. e. ( X X. Y ) ) |
34 |
|
f1of |
|- ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ( X X. Y ) -1-1-onto-> ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) -> ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ( X X. Y ) --> ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) |
35 |
20 34
|
ax-mp |
|- ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ( X X. Y ) --> ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) |
36 |
35
|
ffvelrni |
|- ( <. A , B >. e. ( X X. Y ) -> ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` <. A , B >. ) e. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) |
37 |
33 36
|
syl |
|- ( ph -> ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` <. A , B >. ) e. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) |
38 |
32 37
|
eqeltrrd |
|- ( ph -> { <. (/) , A >. , <. 1o , B >. } e. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) |
39 |
|
df-ov |
|- ( C ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) D ) = ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` <. C , D >. ) |
40 |
15
|
xpsfval |
|- ( ( C e. X /\ D e. Y ) -> ( C ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) D ) = { <. (/) , C >. , <. 1o , D >. } ) |
41 |
13 14 40
|
syl2anc |
|- ( ph -> ( C ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) D ) = { <. (/) , C >. , <. 1o , D >. } ) |
42 |
39 41
|
eqtr3id |
|- ( ph -> ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` <. C , D >. ) = { <. (/) , C >. , <. 1o , D >. } ) |
43 |
13 14
|
opelxpd |
|- ( ph -> <. C , D >. e. ( X X. Y ) ) |
44 |
35
|
ffvelrni |
|- ( <. C , D >. e. ( X X. Y ) -> ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` <. C , D >. ) e. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) |
45 |
43 44
|
syl |
|- ( ph -> ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` <. C , D >. ) e. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) |
46 |
42 45
|
eqeltrrd |
|- ( ph -> { <. (/) , C >. , <. 1o , D >. } e. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) |
47 |
18 19 22 23 24 6 28 38 46
|
imasdsf1o |
|- ( ph -> ( ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` { <. (/) , A >. , <. 1o , B >. } ) P ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` { <. (/) , C >. , <. 1o , D >. } ) ) = ( { <. (/) , A >. , <. 1o , B >. } ( ( dist ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) |` ( ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) X. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) ) { <. (/) , C >. , <. 1o , D >. } ) ) |
48 |
38 46
|
ovresd |
|- ( ph -> ( { <. (/) , A >. , <. 1o , B >. } ( ( dist ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) |` ( ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) X. ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ) ) { <. (/) , C >. , <. 1o , D >. } ) = ( { <. (/) , A >. , <. 1o , B >. } ( dist ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) { <. (/) , C >. , <. 1o , D >. } ) ) |
49 |
47 48
|
eqtrd |
|- ( ph -> ( ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` { <. (/) , A >. , <. 1o , B >. } ) P ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` { <. (/) , C >. , <. 1o , D >. } ) ) = ( { <. (/) , A >. , <. 1o , B >. } ( dist ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) { <. (/) , C >. , <. 1o , D >. } ) ) |
50 |
|
f1ocnvfv |
|- ( ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ( X X. Y ) -1-1-onto-> ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) /\ <. A , B >. e. ( X X. Y ) ) -> ( ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` <. A , B >. ) = { <. (/) , A >. , <. 1o , B >. } -> ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` { <. (/) , A >. , <. 1o , B >. } ) = <. A , B >. ) ) |
51 |
20 33 50
|
sylancr |
|- ( ph -> ( ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` <. A , B >. ) = { <. (/) , A >. , <. 1o , B >. } -> ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` { <. (/) , A >. , <. 1o , B >. } ) = <. A , B >. ) ) |
52 |
32 51
|
mpd |
|- ( ph -> ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` { <. (/) , A >. , <. 1o , B >. } ) = <. A , B >. ) |
53 |
|
f1ocnvfv |
|- ( ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) : ( X X. Y ) -1-1-onto-> ran ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) /\ <. C , D >. e. ( X X. Y ) ) -> ( ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` <. C , D >. ) = { <. (/) , C >. , <. 1o , D >. } -> ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` { <. (/) , C >. , <. 1o , D >. } ) = <. C , D >. ) ) |
54 |
20 43 53
|
sylancr |
|- ( ph -> ( ( ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` <. C , D >. ) = { <. (/) , C >. , <. 1o , D >. } -> ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` { <. (/) , C >. , <. 1o , D >. } ) = <. C , D >. ) ) |
55 |
42 54
|
mpd |
|- ( ph -> ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` { <. (/) , C >. , <. 1o , D >. } ) = <. C , D >. ) |
56 |
52 55
|
oveq12d |
|- ( ph -> ( ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` { <. (/) , A >. , <. 1o , B >. } ) P ( `' ( x e. X , y e. Y |-> { <. (/) , x >. , <. 1o , y >. } ) ` { <. (/) , C >. , <. 1o , D >. } ) ) = ( <. A , B >. P <. C , D >. ) ) |
57 |
|
eqid |
|- ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) = ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) |
58 |
|
fvexd |
|- ( ph -> ( Scalar ` R ) e. _V ) |
59 |
|
2on |
|- 2o e. On |
60 |
59
|
a1i |
|- ( ph -> 2o e. On ) |
61 |
|
fnpr2o |
|- ( ( R e. V /\ S e. W ) -> { <. (/) , R >. , <. 1o , S >. } Fn 2o ) |
62 |
4 5 61
|
syl2anc |
|- ( ph -> { <. (/) , R >. , <. 1o , S >. } Fn 2o ) |
63 |
38 19
|
eleqtrd |
|- ( ph -> { <. (/) , A >. , <. 1o , B >. } e. ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) ) |
64 |
46 19
|
eleqtrd |
|- ( ph -> { <. (/) , C >. , <. 1o , D >. } e. ( Base ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) ) |
65 |
|
eqid |
|- ( dist ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) = ( dist ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) |
66 |
17 57 58 60 62 63 64 65
|
prdsdsval |
|- ( ph -> ( { <. (/) , A >. , <. 1o , B >. } ( dist ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) { <. (/) , C >. , <. 1o , D >. } ) = sup ( ( ran ( k e. 2o |-> ( ( { <. (/) , A >. , <. 1o , B >. } ` k ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , C >. , <. 1o , D >. } ` k ) ) ) u. { 0 } ) , RR* , < ) ) |
67 |
|
df2o3 |
|- 2o = { (/) , 1o } |
68 |
67
|
rexeqi |
|- ( E. k e. 2o x = ( ( { <. (/) , A >. , <. 1o , B >. } ` k ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , C >. , <. 1o , D >. } ` k ) ) <-> E. k e. { (/) , 1o } x = ( ( { <. (/) , A >. , <. 1o , B >. } ` k ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , C >. , <. 1o , D >. } ` k ) ) ) |
69 |
|
0ex |
|- (/) e. _V |
70 |
|
1oex |
|- 1o e. _V |
71 |
|
2fveq3 |
|- ( k = (/) -> ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) = ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` (/) ) ) ) |
72 |
|
fveq2 |
|- ( k = (/) -> ( { <. (/) , A >. , <. 1o , B >. } ` k ) = ( { <. (/) , A >. , <. 1o , B >. } ` (/) ) ) |
73 |
|
fveq2 |
|- ( k = (/) -> ( { <. (/) , C >. , <. 1o , D >. } ` k ) = ( { <. (/) , C >. , <. 1o , D >. } ` (/) ) ) |
74 |
71 72 73
|
oveq123d |
|- ( k = (/) -> ( ( { <. (/) , A >. , <. 1o , B >. } ` k ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , C >. , <. 1o , D >. } ` k ) ) = ( ( { <. (/) , A >. , <. 1o , B >. } ` (/) ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` (/) ) ) ( { <. (/) , C >. , <. 1o , D >. } ` (/) ) ) ) |
75 |
74
|
eqeq2d |
|- ( k = (/) -> ( x = ( ( { <. (/) , A >. , <. 1o , B >. } ` k ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , C >. , <. 1o , D >. } ` k ) ) <-> x = ( ( { <. (/) , A >. , <. 1o , B >. } ` (/) ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` (/) ) ) ( { <. (/) , C >. , <. 1o , D >. } ` (/) ) ) ) ) |
76 |
|
2fveq3 |
|- ( k = 1o -> ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) = ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) ) ) |
77 |
|
fveq2 |
|- ( k = 1o -> ( { <. (/) , A >. , <. 1o , B >. } ` k ) = ( { <. (/) , A >. , <. 1o , B >. } ` 1o ) ) |
78 |
|
fveq2 |
|- ( k = 1o -> ( { <. (/) , C >. , <. 1o , D >. } ` k ) = ( { <. (/) , C >. , <. 1o , D >. } ` 1o ) ) |
79 |
76 77 78
|
oveq123d |
|- ( k = 1o -> ( ( { <. (/) , A >. , <. 1o , B >. } ` k ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , C >. , <. 1o , D >. } ` k ) ) = ( ( { <. (/) , A >. , <. 1o , B >. } ` 1o ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) ) ( { <. (/) , C >. , <. 1o , D >. } ` 1o ) ) ) |
80 |
79
|
eqeq2d |
|- ( k = 1o -> ( x = ( ( { <. (/) , A >. , <. 1o , B >. } ` k ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , C >. , <. 1o , D >. } ` k ) ) <-> x = ( ( { <. (/) , A >. , <. 1o , B >. } ` 1o ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) ) ( { <. (/) , C >. , <. 1o , D >. } ` 1o ) ) ) ) |
81 |
69 70 75 80
|
rexpr |
|- ( E. k e. { (/) , 1o } x = ( ( { <. (/) , A >. , <. 1o , B >. } ` k ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , C >. , <. 1o , D >. } ` k ) ) <-> ( x = ( ( { <. (/) , A >. , <. 1o , B >. } ` (/) ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` (/) ) ) ( { <. (/) , C >. , <. 1o , D >. } ` (/) ) ) \/ x = ( ( { <. (/) , A >. , <. 1o , B >. } ` 1o ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) ) ( { <. (/) , C >. , <. 1o , D >. } ` 1o ) ) ) ) |
82 |
68 81
|
bitri |
|- ( E. k e. 2o x = ( ( { <. (/) , A >. , <. 1o , B >. } ` k ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , C >. , <. 1o , D >. } ` k ) ) <-> ( x = ( ( { <. (/) , A >. , <. 1o , B >. } ` (/) ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` (/) ) ) ( { <. (/) , C >. , <. 1o , D >. } ` (/) ) ) \/ x = ( ( { <. (/) , A >. , <. 1o , B >. } ` 1o ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) ) ( { <. (/) , C >. , <. 1o , D >. } ` 1o ) ) ) ) |
83 |
|
fvpr0o |
|- ( R e. V -> ( { <. (/) , R >. , <. 1o , S >. } ` (/) ) = R ) |
84 |
4 83
|
syl |
|- ( ph -> ( { <. (/) , R >. , <. 1o , S >. } ` (/) ) = R ) |
85 |
84
|
fveq2d |
|- ( ph -> ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` (/) ) ) = ( dist ` R ) ) |
86 |
|
fvpr0o |
|- ( A e. X -> ( { <. (/) , A >. , <. 1o , B >. } ` (/) ) = A ) |
87 |
11 86
|
syl |
|- ( ph -> ( { <. (/) , A >. , <. 1o , B >. } ` (/) ) = A ) |
88 |
|
fvpr0o |
|- ( C e. X -> ( { <. (/) , C >. , <. 1o , D >. } ` (/) ) = C ) |
89 |
13 88
|
syl |
|- ( ph -> ( { <. (/) , C >. , <. 1o , D >. } ` (/) ) = C ) |
90 |
85 87 89
|
oveq123d |
|- ( ph -> ( ( { <. (/) , A >. , <. 1o , B >. } ` (/) ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` (/) ) ) ( { <. (/) , C >. , <. 1o , D >. } ` (/) ) ) = ( A ( dist ` R ) C ) ) |
91 |
7
|
oveqi |
|- ( A M C ) = ( A ( ( dist ` R ) |` ( X X. X ) ) C ) |
92 |
11 13
|
ovresd |
|- ( ph -> ( A ( ( dist ` R ) |` ( X X. X ) ) C ) = ( A ( dist ` R ) C ) ) |
93 |
91 92
|
eqtrid |
|- ( ph -> ( A M C ) = ( A ( dist ` R ) C ) ) |
94 |
90 93
|
eqtr4d |
|- ( ph -> ( ( { <. (/) , A >. , <. 1o , B >. } ` (/) ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` (/) ) ) ( { <. (/) , C >. , <. 1o , D >. } ` (/) ) ) = ( A M C ) ) |
95 |
94
|
eqeq2d |
|- ( ph -> ( x = ( ( { <. (/) , A >. , <. 1o , B >. } ` (/) ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` (/) ) ) ( { <. (/) , C >. , <. 1o , D >. } ` (/) ) ) <-> x = ( A M C ) ) ) |
96 |
|
fvpr1o |
|- ( S e. W -> ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) = S ) |
97 |
5 96
|
syl |
|- ( ph -> ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) = S ) |
98 |
97
|
fveq2d |
|- ( ph -> ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) ) = ( dist ` S ) ) |
99 |
|
fvpr1o |
|- ( B e. Y -> ( { <. (/) , A >. , <. 1o , B >. } ` 1o ) = B ) |
100 |
12 99
|
syl |
|- ( ph -> ( { <. (/) , A >. , <. 1o , B >. } ` 1o ) = B ) |
101 |
|
fvpr1o |
|- ( D e. Y -> ( { <. (/) , C >. , <. 1o , D >. } ` 1o ) = D ) |
102 |
14 101
|
syl |
|- ( ph -> ( { <. (/) , C >. , <. 1o , D >. } ` 1o ) = D ) |
103 |
98 100 102
|
oveq123d |
|- ( ph -> ( ( { <. (/) , A >. , <. 1o , B >. } ` 1o ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) ) ( { <. (/) , C >. , <. 1o , D >. } ` 1o ) ) = ( B ( dist ` S ) D ) ) |
104 |
8
|
oveqi |
|- ( B N D ) = ( B ( ( dist ` S ) |` ( Y X. Y ) ) D ) |
105 |
12 14
|
ovresd |
|- ( ph -> ( B ( ( dist ` S ) |` ( Y X. Y ) ) D ) = ( B ( dist ` S ) D ) ) |
106 |
104 105
|
eqtrid |
|- ( ph -> ( B N D ) = ( B ( dist ` S ) D ) ) |
107 |
103 106
|
eqtr4d |
|- ( ph -> ( ( { <. (/) , A >. , <. 1o , B >. } ` 1o ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) ) ( { <. (/) , C >. , <. 1o , D >. } ` 1o ) ) = ( B N D ) ) |
108 |
107
|
eqeq2d |
|- ( ph -> ( x = ( ( { <. (/) , A >. , <. 1o , B >. } ` 1o ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) ) ( { <. (/) , C >. , <. 1o , D >. } ` 1o ) ) <-> x = ( B N D ) ) ) |
109 |
95 108
|
orbi12d |
|- ( ph -> ( ( x = ( ( { <. (/) , A >. , <. 1o , B >. } ` (/) ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` (/) ) ) ( { <. (/) , C >. , <. 1o , D >. } ` (/) ) ) \/ x = ( ( { <. (/) , A >. , <. 1o , B >. } ` 1o ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` 1o ) ) ( { <. (/) , C >. , <. 1o , D >. } ` 1o ) ) ) <-> ( x = ( A M C ) \/ x = ( B N D ) ) ) ) |
110 |
82 109
|
syl5bb |
|- ( ph -> ( E. k e. 2o x = ( ( { <. (/) , A >. , <. 1o , B >. } ` k ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , C >. , <. 1o , D >. } ` k ) ) <-> ( x = ( A M C ) \/ x = ( B N D ) ) ) ) |
111 |
|
eqid |
|- ( k e. 2o |-> ( ( { <. (/) , A >. , <. 1o , B >. } ` k ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , C >. , <. 1o , D >. } ` k ) ) ) = ( k e. 2o |-> ( ( { <. (/) , A >. , <. 1o , B >. } ` k ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , C >. , <. 1o , D >. } ` k ) ) ) |
112 |
111
|
elrnmpt |
|- ( x e. _V -> ( x e. ran ( k e. 2o |-> ( ( { <. (/) , A >. , <. 1o , B >. } ` k ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , C >. , <. 1o , D >. } ` k ) ) ) <-> E. k e. 2o x = ( ( { <. (/) , A >. , <. 1o , B >. } ` k ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , C >. , <. 1o , D >. } ` k ) ) ) ) |
113 |
112
|
elv |
|- ( x e. ran ( k e. 2o |-> ( ( { <. (/) , A >. , <. 1o , B >. } ` k ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , C >. , <. 1o , D >. } ` k ) ) ) <-> E. k e. 2o x = ( ( { <. (/) , A >. , <. 1o , B >. } ` k ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , C >. , <. 1o , D >. } ` k ) ) ) |
114 |
|
vex |
|- x e. _V |
115 |
114
|
elpr |
|- ( x e. { ( A M C ) , ( B N D ) } <-> ( x = ( A M C ) \/ x = ( B N D ) ) ) |
116 |
110 113 115
|
3bitr4g |
|- ( ph -> ( x e. ran ( k e. 2o |-> ( ( { <. (/) , A >. , <. 1o , B >. } ` k ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , C >. , <. 1o , D >. } ` k ) ) ) <-> x e. { ( A M C ) , ( B N D ) } ) ) |
117 |
116
|
eqrdv |
|- ( ph -> ran ( k e. 2o |-> ( ( { <. (/) , A >. , <. 1o , B >. } ` k ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , C >. , <. 1o , D >. } ` k ) ) ) = { ( A M C ) , ( B N D ) } ) |
118 |
117
|
uneq1d |
|- ( ph -> ( ran ( k e. 2o |-> ( ( { <. (/) , A >. , <. 1o , B >. } ` k ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , C >. , <. 1o , D >. } ` k ) ) ) u. { 0 } ) = ( { ( A M C ) , ( B N D ) } u. { 0 } ) ) |
119 |
|
uncom |
|- ( { ( A M C ) , ( B N D ) } u. { 0 } ) = ( { 0 } u. { ( A M C ) , ( B N D ) } ) |
120 |
118 119
|
eqtrdi |
|- ( ph -> ( ran ( k e. 2o |-> ( ( { <. (/) , A >. , <. 1o , B >. } ` k ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , C >. , <. 1o , D >. } ` k ) ) ) u. { 0 } ) = ( { 0 } u. { ( A M C ) , ( B N D ) } ) ) |
121 |
120
|
supeq1d |
|- ( ph -> sup ( ( ran ( k e. 2o |-> ( ( { <. (/) , A >. , <. 1o , B >. } ` k ) ( dist ` ( { <. (/) , R >. , <. 1o , S >. } ` k ) ) ( { <. (/) , C >. , <. 1o , D >. } ` k ) ) ) u. { 0 } ) , RR* , < ) = sup ( ( { 0 } u. { ( A M C ) , ( B N D ) } ) , RR* , < ) ) |
122 |
|
0xr |
|- 0 e. RR* |
123 |
122
|
a1i |
|- ( ph -> 0 e. RR* ) |
124 |
123
|
snssd |
|- ( ph -> { 0 } C_ RR* ) |
125 |
|
xmetcl |
|- ( ( M e. ( *Met ` X ) /\ A e. X /\ C e. X ) -> ( A M C ) e. RR* ) |
126 |
9 11 13 125
|
syl3anc |
|- ( ph -> ( A M C ) e. RR* ) |
127 |
|
xmetcl |
|- ( ( N e. ( *Met ` Y ) /\ B e. Y /\ D e. Y ) -> ( B N D ) e. RR* ) |
128 |
10 12 14 127
|
syl3anc |
|- ( ph -> ( B N D ) e. RR* ) |
129 |
126 128
|
prssd |
|- ( ph -> { ( A M C ) , ( B N D ) } C_ RR* ) |
130 |
|
xrltso |
|- < Or RR* |
131 |
|
supsn |
|- ( ( < Or RR* /\ 0 e. RR* ) -> sup ( { 0 } , RR* , < ) = 0 ) |
132 |
130 122 131
|
mp2an |
|- sup ( { 0 } , RR* , < ) = 0 |
133 |
|
supxrcl |
|- ( { ( A M C ) , ( B N D ) } C_ RR* -> sup ( { ( A M C ) , ( B N D ) } , RR* , < ) e. RR* ) |
134 |
129 133
|
syl |
|- ( ph -> sup ( { ( A M C ) , ( B N D ) } , RR* , < ) e. RR* ) |
135 |
|
xmetge0 |
|- ( ( M e. ( *Met ` X ) /\ A e. X /\ C e. X ) -> 0 <_ ( A M C ) ) |
136 |
9 11 13 135
|
syl3anc |
|- ( ph -> 0 <_ ( A M C ) ) |
137 |
|
ovex |
|- ( A M C ) e. _V |
138 |
137
|
prid1 |
|- ( A M C ) e. { ( A M C ) , ( B N D ) } |
139 |
|
supxrub |
|- ( ( { ( A M C ) , ( B N D ) } C_ RR* /\ ( A M C ) e. { ( A M C ) , ( B N D ) } ) -> ( A M C ) <_ sup ( { ( A M C ) , ( B N D ) } , RR* , < ) ) |
140 |
129 138 139
|
sylancl |
|- ( ph -> ( A M C ) <_ sup ( { ( A M C ) , ( B N D ) } , RR* , < ) ) |
141 |
123 126 134 136 140
|
xrletrd |
|- ( ph -> 0 <_ sup ( { ( A M C ) , ( B N D ) } , RR* , < ) ) |
142 |
132 141
|
eqbrtrid |
|- ( ph -> sup ( { 0 } , RR* , < ) <_ sup ( { ( A M C ) , ( B N D ) } , RR* , < ) ) |
143 |
|
supxrun |
|- ( ( { 0 } C_ RR* /\ { ( A M C ) , ( B N D ) } C_ RR* /\ sup ( { 0 } , RR* , < ) <_ sup ( { ( A M C ) , ( B N D ) } , RR* , < ) ) -> sup ( ( { 0 } u. { ( A M C ) , ( B N D ) } ) , RR* , < ) = sup ( { ( A M C ) , ( B N D ) } , RR* , < ) ) |
144 |
124 129 142 143
|
syl3anc |
|- ( ph -> sup ( ( { 0 } u. { ( A M C ) , ( B N D ) } ) , RR* , < ) = sup ( { ( A M C ) , ( B N D ) } , RR* , < ) ) |
145 |
66 121 144
|
3eqtrd |
|- ( ph -> ( { <. (/) , A >. , <. 1o , B >. } ( dist ` ( ( Scalar ` R ) Xs_ { <. (/) , R >. , <. 1o , S >. } ) ) { <. (/) , C >. , <. 1o , D >. } ) = sup ( { ( A M C ) , ( B N D ) } , RR* , < ) ) |
146 |
49 56 145
|
3eqtr3d |
|- ( ph -> ( <. A , B >. P <. C , D >. ) = sup ( { ( A M C ) , ( B N D ) } , RR* , < ) ) |