prdsdsval2

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

	Ref	Expression
Hypotheses	prdsbasmpt2.y	$⊢ Y = S ⨉_{𝑠} (x \in I ⟼ R)$
	prdsbasmpt2.b	$⊢ B = {Base}_{Y}$
	prdsbasmpt2.s	$⊢ φ \to S \in V$
	prdsbasmpt2.i	$⊢ φ \to I \in W$
	prdsbasmpt2.r	$⊢ φ \to \forall x \in I R \in X$
	prdsdsval2.f	$⊢ φ \to F \in B$
	prdsdsval2.g	$⊢ φ \to G \in B$
	prdsdsval2.e	$⊢ E = dist (R)$
	prdsdsval2.d	$⊢ D = dist (Y)$
Assertion	prdsdsval2	$⊢ φ \to F D G = sup (ran (x \in I ⟼ F (x) E G (x)) \cup \{0\} ℝ^{*} <)$

Proof

Step	Hyp	Ref	Expression
1		prdsbasmpt2.y	$⊢ Y = S ⨉_{𝑠} (x \in I ⟼ R)$
2		prdsbasmpt2.b	$⊢ B = {Base}_{Y}$
3		prdsbasmpt2.s	$⊢ φ \to S \in V$
4		prdsbasmpt2.i	$⊢ φ \to I \in W$
5		prdsbasmpt2.r	$⊢ φ \to \forall x \in I R \in X$
6		prdsdsval2.f	$⊢ φ \to F \in B$
7		prdsdsval2.g	$⊢ φ \to G \in B$
8		prdsdsval2.e	$⊢ E = dist (R)$
9		prdsdsval2.d	$⊢ D = dist (Y)$
10		eqid	$⊢ (x \in I ⟼ R) = (x \in I ⟼ R)$
11	10	fnmpt	$⊢ \forall x \in I R \in X \to (x \in I ⟼ R) Fn I$
12	5 11	syl	$⊢ φ \to (x \in I ⟼ R) Fn I$
13	1 2 3 4 12 6 7 9	prdsdsval	$⊢ φ \to F D G = sup (ran (y \in I ⟼ F (y) dist ((x \in I ⟼ R) (y)) G (y)) \cup \{0\} ℝ^{*} <)$
14		nfcv	$⊢ \underline{Ⅎ} x F (y)$
15		nfcv	$⊢ \underline{Ⅎ} x dist$
16		nffvmpt1	$⊢ \underline{Ⅎ} x (x \in I ⟼ R) (y)$
17	15 16	nffv	$⊢ \underline{Ⅎ} x dist ((x \in I ⟼ R) (y))$
18		nfcv	$⊢ \underline{Ⅎ} x G (y)$
19	14 17 18	nfov	$⊢ \underline{Ⅎ} x (F (y) dist ((x \in I ⟼ R) (y)) G (y))$
20		nfcv	$⊢ \underline{Ⅎ} y (F (x) dist ((x \in I ⟼ R) (x)) G (x))$
21		2fveq3	$⊢ y = x \to dist ((x \in I ⟼ R) (y)) = dist ((x \in I ⟼ R) (x))$
22		fveq2	$⊢ y = x \to F (y) = F (x)$
23		fveq2	$⊢ y = x \to G (y) = G (x)$
24	21 22 23	oveq123d	$⊢ y = x \to F (y) dist ((x \in I ⟼ R) (y)) G (y) = F (x) dist ((x \in I ⟼ R) (x)) G (x)$
25	19 20 24	cbvmpt	$⊢ (y \in I ⟼ F (y) dist ((x \in I ⟼ R) (y)) G (y)) = (x \in I ⟼ F (x) dist ((x \in I ⟼ R) (x)) G (x))$
26		eqidd	$⊢ φ \to I = I$
27	10	fvmpt2	$⊢ (x \in I \land R \in X) \to (x \in I ⟼ R) (x) = R$
28	27	fveq2d	$⊢ (x \in I \land R \in X) \to dist ((x \in I ⟼ R) (x)) = dist (R)$
29	28 8	syl6eqr	$⊢ (x \in I \land R \in X) \to dist ((x \in I ⟼ R) (x)) = E$
30	29	oveqd	$⊢ (x \in I \land R \in X) \to F (x) dist ((x \in I ⟼ R) (x)) G (x) = F (x) E G (x)$
31	30	ralimiaa	$⊢ \forall x \in I R \in X \to \forall x \in I F (x) dist ((x \in I ⟼ R) (x)) G (x) = F (x) E G (x)$
32	5 31	syl	$⊢ φ \to \forall x \in I F (x) dist ((x \in I ⟼ R) (x)) G (x) = F (x) E G (x)$
33		mpteq12	$⊢ (I = I \land \forall x \in I F (x) dist ((x \in I ⟼ R) (x)) G (x) = F (x) E G (x)) \to (x \in I ⟼ F (x) dist ((x \in I ⟼ R) (x)) G (x)) = (x \in I ⟼ F (x) E G (x))$
34	26 32 33	syl2anc	$⊢ φ \to (x \in I ⟼ F (x) dist ((x \in I ⟼ R) (x)) G (x)) = (x \in I ⟼ F (x) E G (x))$
35	25 34	syl5eq	$⊢ φ \to (y \in I ⟼ F (y) dist ((x \in I ⟼ R) (y)) G (y)) = (x \in I ⟼ F (x) E G (x))$
36	35	rneqd	$⊢ φ \to ran (y \in I ⟼ F (y) dist ((x \in I ⟼ R) (y)) G (y)) = ran (x \in I ⟼ F (x) E G (x))$
37	36	uneq1d	$⊢ φ \to ran (y \in I ⟼ F (y) dist ((x \in I ⟼ R) (y)) G (y)) \cup \{0\} = ran (x \in I ⟼ F (x) E G (x)) \cup \{0\}$
38	37	supeq1d	$⊢ φ \to sup (ran (y \in I ⟼ F (y) dist ((x \in I ⟼ R) (y)) G (y)) \cup \{0\} ℝ^{} <) = sup (ran (x \in I ⟼ F (x) E G (x)) \cup \{0\} ℝ^{} <)$
39	13 38	eqtrd	$⊢ φ \to F D G = sup (ran (x \in I ⟼ F (x) E G (x)) \cup \{0\} ℝ^{*} <)$

Metamath Proof Explorer

Theorem prdsdsval2

Proof