prdsdsval

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

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

Proof

Step	Hyp	Ref	Expression
1		prdsbasmpt.y	$⊢ Y = S ⨉_{𝑠} R$
2		prdsbasmpt.b	$⊢ B = {Base}_{Y}$
3		prdsbasmpt.s	$⊢ φ \to S \in V$
4		prdsbasmpt.i	$⊢ φ \to I \in W$
5		prdsbasmpt.r	$⊢ φ \to R Fn I$
6		prdsplusgval.f	$⊢ φ \to F \in B$
7		prdsplusgval.g	$⊢ φ \to G \in B$
8		prdsdsval.d	$⊢ D = dist (Y)$
9		fnex	$⊢ (R Fn I \land I \in W) \to R \in V$
10	5 4 9	syl2anc	$⊢ φ \to R \in V$
11		fndm	$⊢ R Fn I \to dom R = I$
12	5 11	syl	$⊢ φ \to dom R = I$
13	1 3 10 2 12 8	prdsds	$⊢ φ \to D = (f \in B, g \in B ⟼ sup (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{*} <))$
14		fveq1	$⊢ f = F \to f (x) = F (x)$
15		fveq1	$⊢ g = G \to g (x) = G (x)$
16	14 15	oveqan12d	$⊢ (f = F \land g = G) \to f (x) dist (R (x)) g (x) = F (x) dist (R (x)) G (x)$
17	16	adantl	$⊢ (φ \land (f = F \land g = G)) \to f (x) dist (R (x)) g (x) = F (x) dist (R (x)) G (x)$
18	17	mpteq2dv	$⊢ (φ \land (f = F \land g = G)) \to (x \in I ⟼ f (x) dist (R (x)) g (x)) = (x \in I ⟼ F (x) dist (R (x)) G (x))$
19	18	rneqd	$⊢ (φ \land (f = F \land g = G)) \to ran (x \in I ⟼ f (x) dist (R (x)) g (x)) = ran (x \in I ⟼ F (x) dist (R (x)) G (x))$
20	19	uneq1d	$⊢ (φ \land (f = F \land g = G)) \to ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} = ran (x \in I ⟼ F (x) dist (R (x)) G (x)) \cup \{0\}$
21	20	supeq1d	$⊢ (φ \land (f = F \land g = G)) \to sup (ran (x \in I ⟼ f (x) dist (R (x)) g (x)) \cup \{0\} ℝ^{} <) = sup (ran (x \in I ⟼ F (x) dist (R (x)) G (x)) \cup \{0\} ℝ^{} <)$
22		xrltso	$⊢ < Or ℝ^{*}$
23	22	supex	$⊢ sup (ran (x \in I ⟼ F (x) dist (R (x)) G (x)) \cup \{0\} ℝ^{*} <) \in V$
24	23	a1i	$⊢ φ \to sup (ran (x \in I ⟼ F (x) dist (R (x)) G (x)) \cup \{0\} ℝ^{*} <) \in V$
25	13 21 6 7 24	ovmpod	$⊢ φ \to F D G = sup (ran (x \in I ⟼ F (x) dist (R (x)) G (x)) \cup \{0\} ℝ^{*} <)$

Metamath Proof Explorer

Theorem prdsdsval

Proof