prdsdsf

Description: The product metric is a function into the nonnegative extended reals. In general this means that it is not a metric but rather an *extended* metric (even when all the factors are metrics), but it will be a metric when restricted to regions where it does not take infinite values. (Contributed by Mario Carneiro, 20-Aug-2015)

	Ref	Expression
Hypotheses	prdsdsf.y	$⊢ Y = S ⨉_{𝑠} (x \in I ⟼ R)$
	prdsdsf.b	$⊢ B = {Base}_{Y}$
	prdsdsf.v	$⊢ V = {Base}_{R}$
	prdsdsf.e	$⊢ E = {dist (R) ↾}_{(V \times V)}$
	prdsdsf.d	$⊢ D = dist (Y)$
	prdsdsf.s	$⊢ φ \to S \in W$
	prdsdsf.i	$⊢ φ \to I \in X$
	prdsdsf.r	$⊢ (φ \land x \in I) \to R \in Z$
	prdsdsf.m	$⊢ (φ \land x \in I) \to E \in ∞Met (V)$
Assertion	prdsdsf	$⊢ φ \to D : B \times B ⟶ [0, +∞]$

Proof

Step	Hyp	Ref	Expression
1		prdsdsf.y	$⊢ Y = S ⨉_{𝑠} (x \in I ⟼ R)$
2		prdsdsf.b	$⊢ B = {Base}_{Y}$
3		prdsdsf.v	$⊢ V = {Base}_{R}$
4		prdsdsf.e	$⊢ E = {dist (R) ↾}_{(V \times V)}$
5		prdsdsf.d	$⊢ D = dist (Y)$
6		prdsdsf.s	$⊢ φ \to S \in W$
7		prdsdsf.i	$⊢ φ \to I \in X$
8		prdsdsf.r	$⊢ (φ \land x \in I) \to R \in Z$
9		prdsdsf.m	$⊢ (φ \land x \in I) \to E \in ∞Met (V)$
10		simpr	$⊢ ((φ \land (f \in B \land g \in B)) \land y \in I) \to y \in I$
11	8	elexd	$⊢ (φ \land x \in I) \to R \in V$
12	11	ralrimiva	$⊢ φ \to \forall x \in I R \in V$
13	12	adantr	$⊢ (φ \land (f \in B \land g \in B)) \to \forall x \in I R \in V$
14		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ y / x ⦌ R$
15	14	nfel1	$⊢ Ⅎ x ⦋ y / x ⦌ R \in V$
16		csbeq1a	$⊢ x = y \to R = ⦋ y / x ⦌ R$
17	16	eleq1d	$⊢ x = y \to (R \in V \leftrightarrow ⦋ y / x ⦌ R \in V)$
18	15 17	rspc	$⊢ y \in I \to (\forall x \in I R \in V \to ⦋ y / x ⦌ R \in V)$
19	13 18	mpan9	$⊢ ((φ \land (f \in B \land g \in B)) \land y \in I) \to ⦋ y / x ⦌ R \in V$
20		eqid	$⊢ (x \in I ⟼ R) = (x \in I ⟼ R)$
21	20	fvmpts	$⊢ (y \in I \land ⦋ y / x ⦌ R \in V) \to (x \in I ⟼ R) (y) = ⦋ y / x ⦌ R$
22	10 19 21	syl2anc	$⊢ ((φ \land (f \in B \land g \in B)) \land y \in I) \to (x \in I ⟼ R) (y) = ⦋ y / x ⦌ R$
23	22	fveq2d	$⊢ ((φ \land (f \in B \land g \in B)) \land y \in I) \to dist ((x \in I ⟼ R) (y)) = dist (⦋ y / x ⦌ R)$
24	23	oveqd	$⊢ ((φ \land (f \in B \land g \in B)) \land y \in I) \to f (y) dist ((x \in I ⟼ R) (y)) g (y) = f (y) dist (⦋ y / x ⦌ R) g (y)$
25	6	adantr	$⊢ (φ \land (f \in B \land g \in B)) \to S \in W$
26	7	adantr	$⊢ (φ \land (f \in B \land g \in B)) \to I \in X$
27		simprl	$⊢ (φ \land (f \in B \land g \in B)) \to f \in B$
28	1 2 25 26 13 3 27	prdsbascl	$⊢ (φ \land (f \in B \land g \in B)) \to \forall x \in I f (x) \in V$
29		nfcsb1v	$⊢ \underline{Ⅎ} x ⦋ y / x ⦌ V$
30	29	nfel2	$⊢ Ⅎ x f (y) \in ⦋ y / x ⦌ V$
31		fveq2	$⊢ x = y \to f (x) = f (y)$
32		csbeq1a	$⊢ x = y \to V = ⦋ y / x ⦌ V$
33	31 32	eleq12d	$⊢ x = y \to (f (x) \in V \leftrightarrow f (y) \in ⦋ y / x ⦌ V)$
34	30 33	rspc	$⊢ y \in I \to (\forall x \in I f (x) \in V \to f (y) \in ⦋ y / x ⦌ V)$
35	28 34	mpan9	$⊢ ((φ \land (f \in B \land g \in B)) \land y \in I) \to f (y) \in ⦋ y / x ⦌ V$
36		simprr	$⊢ (φ \land (f \in B \land g \in B)) \to g \in B$
37	1 2 25 26 13 3 36	prdsbascl	$⊢ (φ \land (f \in B \land g \in B)) \to \forall x \in I g (x) \in V$
38	29	nfel2	$⊢ Ⅎ x g (y) \in ⦋ y / x ⦌ V$
39		fveq2	$⊢ x = y \to g (x) = g (y)$
40	39 32	eleq12d	$⊢ x = y \to (g (x) \in V \leftrightarrow g (y) \in ⦋ y / x ⦌ V)$
41	38 40	rspc	$⊢ y \in I \to (\forall x \in I g (x) \in V \to g (y) \in ⦋ y / x ⦌ V)$
42	37 41	mpan9	$⊢ ((φ \land (f \in B \land g \in B)) \land y \in I) \to g (y) \in ⦋ y / x ⦌ V$
43	35 42	ovresd	$⊢ ((φ \land (f \in B \land g \in B)) \land y \in I) \to f (y) ({dist (⦋ y / x ⦌ R) ↾}_{(⦋ y / x ⦌ V \times ⦋ y / x ⦌ V)}) g (y) = f (y) dist (⦋ y / x ⦌ R) g (y)$
44	24 43	eqtr4d	$⊢ ((φ \land (f \in B \land g \in B)) \land y \in I) \to f (y) dist ((x \in I ⟼ R) (y)) g (y) = f (y) ({dist (⦋ y / x ⦌ R) ↾}_{(⦋ y / x ⦌ V \times ⦋ y / x ⦌ V)}) g (y)$
45	9	ralrimiva	$⊢ φ \to \forall x \in I E \in ∞Met (V)$
46	45	adantr	$⊢ (φ \land (f \in B \land g \in B)) \to \forall x \in I E \in ∞Met (V)$
47		nfcv	$⊢ \underline{Ⅎ} x dist$
48	47 14	nffv	$⊢ \underline{Ⅎ} x dist (⦋ y / x ⦌ R)$
49	29 29	nfxp	$⊢ \underline{Ⅎ} x (⦋ y / x ⦌ V \times ⦋ y / x ⦌ V)$
50	48 49	nfres	$⊢ \underline{Ⅎ} x ({dist (⦋ y / x ⦌ R) ↾}_{(⦋ y / x ⦌ V \times ⦋ y / x ⦌ V)})$
51		nfcv	$⊢ \underline{Ⅎ} x ∞Met$
52	51 29	nffv	$⊢ \underline{Ⅎ} x ∞Met (⦋ y / x ⦌ V)$
53	50 52	nfel	$⊢ Ⅎ x {dist (⦋ y / x ⦌ R) ↾}_{(⦋ y / x ⦌ V \times ⦋ y / x ⦌ V)} \in ∞Met (⦋ y / x ⦌ V)$
54	16	fveq2d	$⊢ x = y \to dist (R) = dist (⦋ y / x ⦌ R)$
55	32	sqxpeqd	$⊢ x = y \to V \times V = ⦋ y / x ⦌ V \times ⦋ y / x ⦌ V$
56	54 55	reseq12d	$⊢ x = y \to {dist (R) ↾}_{(V \times V)} = {dist (⦋ y / x ⦌ R) ↾}_{(⦋ y / x ⦌ V \times ⦋ y / x ⦌ V)}$
57	4 56	syl5eq	$⊢ x = y \to E = {dist (⦋ y / x ⦌ R) ↾}_{(⦋ y / x ⦌ V \times ⦋ y / x ⦌ V)}$
58	32	fveq2d	$⊢ x = y \to ∞Met (V) = ∞Met (⦋ y / x ⦌ V)$
59	57 58	eleq12d	$⊢ x = y \to (E \in ∞Met (V) \leftrightarrow {dist (⦋ y / x ⦌ R) ↾}_{(⦋ y / x ⦌ V \times ⦋ y / x ⦌ V)} \in ∞Met (⦋ y / x ⦌ V))$
60	53 59	rspc	$⊢ y \in I \to (\forall x \in I E \in ∞Met (V) \to {dist (⦋ y / x ⦌ R) ↾}_{(⦋ y / x ⦌ V \times ⦋ y / x ⦌ V)} \in ∞Met (⦋ y / x ⦌ V))$
61	46 60	mpan9	$⊢ ((φ \land (f \in B \land g \in B)) \land y \in I) \to {dist (⦋ y / x ⦌ R) ↾}_{(⦋ y / x ⦌ V \times ⦋ y / x ⦌ V)} \in ∞Met (⦋ y / x ⦌ V)$
62		xmetcl	$⊢ ({dist (⦋ y / x ⦌ R) ↾}_{(⦋ y / x ⦌ V \times ⦋ y / x ⦌ V)} \in ∞Met (⦋ y / x ⦌ V) \land f (y) \in ⦋ y / x ⦌ V \land g (y) \in ⦋ y / x ⦌ V) \to f (y) ({dist (⦋ y / x ⦌ R) ↾}_{(⦋ y / x ⦌ V \times ⦋ y / x ⦌ V)}) g (y) \in ℝ^{*}$
63	61 35 42 62	syl3anc	$⊢ ((φ \land (f \in B \land g \in B)) \land y \in I) \to f (y) ({dist (⦋ y / x ⦌ R) ↾}_{(⦋ y / x ⦌ V \times ⦋ y / x ⦌ V)}) g (y) \in ℝ^{*}$
64	44 63	eqeltrd	$⊢ ((φ \land (f \in B \land g \in B)) \land y \in I) \to f (y) dist ((x \in I ⟼ R) (y)) g (y) \in ℝ^{*}$
65	64	fmpttd	$⊢ (φ \land (f \in B \land g \in B)) \to (y \in I ⟼ f (y) dist ((x \in I ⟼ R) (y)) g (y)) : I ⟶ ℝ^{*}$
66	65	frnd	$⊢ (φ \land (f \in B \land g \in B)) \to ran (y \in I ⟼ f (y) dist ((x \in I ⟼ R) (y)) g (y)) \subseteq ℝ^{*}$
67		0xr	$⊢ 0 \in ℝ^{*}$
68	67	a1i	$⊢ (φ \land (f \in B \land g \in B)) \to 0 \in ℝ^{*}$
69	68	snssd	$⊢ (φ \land (f \in B \land g \in B)) \to \{0\} \subseteq ℝ^{*}$
70	66 69	unssd	$⊢ (φ \land (f \in B \land g \in B)) \to ran (y \in I ⟼ f (y) dist ((x \in I ⟼ R) (y)) g (y)) \cup \{0\} \subseteq ℝ^{*}$
71		supxrcl	$⊢ ran (y \in I ⟼ f (y) dist ((x \in I ⟼ R) (y)) g (y)) \cup \{0\} \subseteq ℝ^{} \to sup (ran (y \in I ⟼ f (y) dist ((x \in I ⟼ R) (y)) g (y)) \cup \{0\} ℝ^{} <) \in ℝ^{*}$
72	70 71	syl	$⊢ (φ \land (f \in B \land g \in B)) \to sup (ran (y \in I ⟼ f (y) dist ((x \in I ⟼ R) (y)) g (y)) \cup \{0\} ℝ^{} <) \in ℝ^{}$
73		ssun2	$⊢ \{0\} \subseteq ran (y \in I ⟼ f (y) dist ((x \in I ⟼ R) (y)) g (y)) \cup \{0\}$
74		c0ex	$⊢ 0 \in V$
75	74	snss	$⊢ 0 \in (ran (y \in I ⟼ f (y) dist ((x \in I ⟼ R) (y)) g (y)) \cup \{0\}) \leftrightarrow \{0\} \subseteq ran (y \in I ⟼ f (y) dist ((x \in I ⟼ R) (y)) g (y)) \cup \{0\}$
76	73 75	mpbir	$⊢ 0 \in (ran (y \in I ⟼ f (y) dist ((x \in I ⟼ R) (y)) g (y)) \cup \{0\})$
77		supxrub	$⊢ (ran (y \in I ⟼ f (y) dist ((x \in I ⟼ R) (y)) g (y)) \cup \{0\} \subseteq ℝ^{} \land 0 \in (ran (y \in I ⟼ f (y) dist ((x \in I ⟼ R) (y)) g (y)) \cup \{0\})) \to 0 \leq sup (ran (y \in I ⟼ f (y) dist ((x \in I ⟼ R) (y)) g (y)) \cup \{0\} ℝ^{} <)$
78	70 76 77	sylancl	$⊢ (φ \land (f \in B \land g \in B)) \to 0 \leq sup (ran (y \in I ⟼ f (y) dist ((x \in I ⟼ R) (y)) g (y)) \cup \{0\} ℝ^{*} <)$
79		elxrge0	$⊢ sup (ran (y \in I ⟼ f (y) dist ((x \in I ⟼ R) (y)) g (y)) \cup \{0\} ℝ^{} <) \in [0, +∞] \leftrightarrow (sup (ran (y \in I ⟼ f (y) dist ((x \in I ⟼ R) (y)) g (y)) \cup \{0\} ℝ^{} <) \in ℝ^{} \land 0 \leq sup (ran (y \in I ⟼ f (y) dist ((x \in I ⟼ R) (y)) g (y)) \cup \{0\} ℝ^{} <))$
80	72 78 79	sylanbrc	$⊢ (φ \land (f \in B \land g \in B)) \to sup (ran (y \in I ⟼ f (y) dist ((x \in I ⟼ R) (y)) g (y)) \cup \{0\} ℝ^{*} <) \in [0, +∞]$
81	80	ralrimivva	$⊢ φ \to \forall f \in B \forall g \in B sup (ran (y \in I ⟼ f (y) dist ((x \in I ⟼ R) (y)) g (y)) \cup \{0\} ℝ^{*} <) \in [0, +∞]$
82		eqid	$⊢ (f \in B, g \in B ⟼ sup (ran (y \in I ⟼ f (y) dist ((x \in I ⟼ R) (y)) g (y)) \cup \{0\} ℝ^{} <)) = (f \in B, g \in B ⟼ sup (ran (y \in I ⟼ f (y) dist ((x \in I ⟼ R) (y)) g (y)) \cup \{0\} ℝ^{} <))$
83	82	fmpo	$⊢ \forall f \in B \forall g \in B sup (ran (y \in I ⟼ f (y) dist ((x \in I ⟼ R) (y)) g (y)) \cup \{0\} ℝ^{} <) \in [0, +∞] \leftrightarrow (f \in B, g \in B ⟼ sup (ran (y \in I ⟼ f (y) dist ((x \in I ⟼ R) (y)) g (y)) \cup \{0\} ℝ^{} <)) : B \times B ⟶ [0, +∞]$
84	81 83	sylib	$⊢ φ \to (f \in B, g \in B ⟼ sup (ran (y \in I ⟼ f (y) dist ((x \in I ⟼ R) (y)) g (y)) \cup \{0\} ℝ^{*} <)) : B \times B ⟶ [0, +∞]$
85	7	mptexd	$⊢ φ \to (x \in I ⟼ R) \in V$
86	8	ralrimiva	$⊢ φ \to \forall x \in I R \in Z$
87		dmmptg	$⊢ \forall x \in I R \in Z \to dom (x \in I ⟼ R) = I$
88	86 87	syl	$⊢ φ \to dom (x \in I ⟼ R) = I$
89	1 6 85 2 88 5	prdsds	$⊢ φ \to D = (f \in B, g \in B ⟼ sup (ran (y \in I ⟼ f (y) dist ((x \in I ⟼ R) (y)) g (y)) \cup \{0\} ℝ^{*} <))$
90	89	feq1d	$⊢ φ \to (D : B \times B ⟶ [0, +∞] \leftrightarrow (f \in B, g \in B ⟼ sup (ran (y \in I ⟼ f (y) dist ((x \in I ⟼ R) (y)) g (y)) \cup \{0\} ℝ^{*} <)) : B \times B ⟶ [0, +∞])$
91	84 90	mpbird	$⊢ φ \to D : B \times B ⟶ [0, +∞]$

Metamath Proof Explorer

Theorem prdsdsf

Proof