prdsdsval3

Description: Value of the metric in a structure product. (Contributed by Mario Carneiro, 27-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$
	prdsdsval3.k	$⊢ K = {Base}_{R}$
	prdsdsval3.e	$⊢ E = {dist (R) ↾}_{(K \times K)}$
	prdsdsval3.d	$⊢ D = dist (Y)$
Assertion	prdsdsval3	$⊢ φ \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		prdsdsval3.k	$⊢ K = {Base}_{R}$
9		prdsdsval3.e	$⊢ E = {dist (R) ↾}_{(K \times K)}$
10		prdsdsval3.d	$⊢ D = dist (Y)$
11		eqid	$⊢ dist (R) = dist (R)$
12	1 2 3 4 5 6 7 11 10	prdsdsval2	$⊢ φ \to F D G = sup (ran (x \in I ⟼ F (x) dist (R) G (x)) \cup \{0\} ℝ^{*} <)$
13		eqidd	$⊢ φ \to I = I$
14	1 2 3 4 5 8 6	prdsbascl	$⊢ φ \to \forall x \in I F (x) \in K$
15	1 2 3 4 5 8 7	prdsbascl	$⊢ φ \to \forall x \in I G (x) \in K$
16	9	oveqi	$⊢ F (x) E G (x) = F (x) ({dist (R) ↾}_{(K \times K)}) G (x)$
17		ovres	$⊢ (F (x) \in K \land G (x) \in K) \to F (x) ({dist (R) ↾}_{(K \times K)}) G (x) = F (x) dist (R) G (x)$
18	16 17	syl5eq	$⊢ (F (x) \in K \land G (x) \in K) \to F (x) E G (x) = F (x) dist (R) G (x)$
19	18	ex	$⊢ F (x) \in K \to (G (x) \in K \to F (x) E G (x) = F (x) dist (R) G (x))$
20	19	ral2imi	$⊢ \forall x \in I F (x) \in K \to (\forall x \in I G (x) \in K \to \forall x \in I F (x) E G (x) = F (x) dist (R) G (x))$
21	14 15 20	sylc	$⊢ φ \to \forall x \in I F (x) E G (x) = F (x) dist (R) G (x)$
22		mpteq12	$⊢ (I = I \land \forall x \in I F (x) E G (x) = F (x) dist (R) G (x)) \to (x \in I ⟼ F (x) E G (x)) = (x \in I ⟼ F (x) dist (R) G (x))$
23	13 21 22	syl2anc	$⊢ φ \to (x \in I ⟼ F (x) E G (x)) = (x \in I ⟼ F (x) dist (R) G (x))$
24	23	rneqd	$⊢ φ \to ran (x \in I ⟼ F (x) E G (x)) = ran (x \in I ⟼ F (x) dist (R) G (x))$
25	24	uneq1d	$⊢ φ \to ran (x \in I ⟼ F (x) E G (x)) \cup \{0\} = ran (x \in I ⟼ F (x) dist (R) G (x)) \cup \{0\}$
26	25	supeq1d	$⊢ φ \to sup (ran (x \in I ⟼ F (x) E G (x)) \cup \{0\} ℝ^{} <) = sup (ran (x \in I ⟼ F (x) dist (R) G (x)) \cup \{0\} ℝ^{} <)$
27	12 26	eqtr4d	$⊢ φ \to F D G = sup (ran (x \in I ⟼ F (x) E G (x)) \cup \{0\} ℝ^{*} <)$

Metamath Proof Explorer

Theorem prdsdsval3

Proof