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* , < ) )