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 \times_{𝑠} S$
	xpsds.x	$⊢ X = {Base}_{R}$
	xpsds.y	$⊢ Y = {Base}_{S}$
	xpsds.1	$⊢ φ \to R \in V$
	xpsds.2	$⊢ φ \to S \in W$
	xpsds.p	$⊢ P = dist (T)$
	xpsds.m	$⊢ M = {dist (R) ↾}_{(X \times X)}$
	xpsds.n	$⊢ N = {dist (S) ↾}_{(Y \times Y)}$
	xpsds.3	$⊢ φ \to M \in ∞Met (X)$
	xpsds.4	$⊢ φ \to N \in ∞Met (Y)$
	xpsds.a	$⊢ φ \to A \in X$
	xpsds.b	$⊢ φ \to B \in Y$
	xpsds.c	$⊢ φ \to C \in X$
	xpsds.d	$⊢ φ \to D \in Y$
Assertion	xpsdsval	$⊢ φ \to ⟨A, B⟩ P ⟨C, D⟩ = sup (\{A M C, B N D\} ℝ^{*} <)$

Proof

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

Metamath Proof Explorer

Theorem xpsdsval

Proof