This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem xpsdsval

Description: Value of the metric in a binary structure product. (Contributed by Mario Carneiro, 20-Aug-2015)

Ref Expression
Hypotheses xpsds.t 
|- T = ( R Xs. S )
xpsds.x 
|- X = ( Base ` R )
xpsds.y 
|- Y = ( Base ` S )
xpsds.1 
|- ( ph -> R e. V )
xpsds.2 
|- ( ph -> S e. W )
xpsds.p 
|- P = ( dist ` T )
xpsds.m 
|- M = ( ( dist ` R ) |` ( X X. X ) )
xpsds.n 
|- N = ( ( dist ` S ) |` ( Y X. Y ) )
xpsds.3 
|- ( ph -> M e. ( *Met ` X ) )
xpsds.4 
|- ( ph -> N e. ( *Met ` Y ) )
xpsds.a 
|- ( ph -> A e. X )
xpsds.b 
|- ( ph -> B e. Y )
xpsds.c 
|- ( ph -> C e. X )
xpsds.d 
|- ( ph -> D e. Y )
Assertion xpsdsval 
|- ( ph -> ( <. A , B >. P <. C , D >. ) = sup ( { ( A M C ) , ( B N D ) } , RR* , < ) )

Proof

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 ffvelcdmi 
 |-  ( <. 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 ffvelcdmi 
 |-  ( <. 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 bitrid 
 |-  ( 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* , < ) )