prdsxmetlem

Description: The product metric is an extended metric. (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	prdsxmetlem	$⊢ φ \to D \in ∞Met (B)$

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	2	fvexi	$⊢ B \in V$
11	10	a1i	$⊢ φ \to B \in V$
12	1 2 3 4 5 6 7 8 9	prdsdsf	$⊢ φ \to D : B \times B ⟶ [0, +∞]$
13		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
14		fss	$⊢ (D : B \times B ⟶ [0, +∞] \land [0, +∞] \subseteq ℝ^{}) \to D : B \times B ⟶ ℝ^{}$
15	12 13 14	sylancl	$⊢ φ \to D : B \times B ⟶ ℝ^{*}$
16	12	fovrnda	$⊢ (φ \land (f \in B \land g \in B)) \to f D g \in [0, +∞]$
17		elxrge0	$⊢ f D g \in [0, +∞] \leftrightarrow (f D g \in ℝ^{*} \land 0 \leq f D g)$
18	17	simprbi	$⊢ f D g \in [0, +∞] \to 0 \leq f D g$
19	16 18	syl	$⊢ (φ \land (f \in B \land g \in B)) \to 0 \leq f D g$
20	6	adantr	$⊢ (φ \land (f \in B \land g \in B)) \to S \in W$
21	7	adantr	$⊢ (φ \land (f \in B \land g \in B)) \to I \in X$
22	8	ralrimiva	$⊢ φ \to \forall x \in I R \in Z$
23	22	adantr	$⊢ (φ \land (f \in B \land g \in B)) \to \forall x \in I R \in Z$
24		simprl	$⊢ (φ \land (f \in B \land g \in B)) \to f \in B$
25		simprr	$⊢ (φ \land (f \in B \land g \in B)) \to g \in B$
26	1 2 20 21 23 24 25 3 4 5	prdsdsval3	$⊢ (φ \land (f \in B \land g \in B)) \to f D g = sup (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} ℝ^{*} <)$
27	26	breq1d	$⊢ (φ \land (f \in B \land g \in B)) \to (f D g \leq 0 \leftrightarrow sup (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} ℝ^{*} <) \leq 0)$
28	9	adantlr	$⊢ ((φ \land (f \in B \land g \in B)) \land x \in I) \to E \in ∞Met (V)$
29	1 2 20 21 23 3 24	prdsbascl	$⊢ (φ \land (f \in B \land g \in B)) \to \forall x \in I f (x) \in V$
30	29	r19.21bi	$⊢ ((φ \land (f \in B \land g \in B)) \land x \in I) \to f (x) \in V$
31	1 2 20 21 23 3 25	prdsbascl	$⊢ (φ \land (f \in B \land g \in B)) \to \forall x \in I g (x) \in V$
32	31	r19.21bi	$⊢ ((φ \land (f \in B \land g \in B)) \land x \in I) \to g (x) \in V$
33		xmetcl	$⊢ (E \in ∞Met (V) \land f (x) \in V \land g (x) \in V) \to f (x) E g (x) \in ℝ^{*}$
34	28 30 32 33	syl3anc	$⊢ ((φ \land (f \in B \land g \in B)) \land x \in I) \to f (x) E g (x) \in ℝ^{*}$
35	34	fmpttd	$⊢ (φ \land (f \in B \land g \in B)) \to (x \in I ⟼ f (x) E g (x)) : I ⟶ ℝ^{*}$
36	35	frnd	$⊢ (φ \land (f \in B \land g \in B)) \to ran (x \in I ⟼ f (x) E g (x)) \subseteq ℝ^{*}$
37		0xr	$⊢ 0 \in ℝ^{*}$
38	37	a1i	$⊢ (φ \land (f \in B \land g \in B)) \to 0 \in ℝ^{*}$
39	38	snssd	$⊢ (φ \land (f \in B \land g \in B)) \to \{0\} \subseteq ℝ^{*}$
40	36 39	unssd	$⊢ (φ \land (f \in B \land g \in B)) \to ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} \subseteq ℝ^{*}$
41		supxrleub	$⊢ (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} \subseteq ℝ^{} \land 0 \in ℝ^{}) \to (sup (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} ℝ^{*} <) \leq 0 \leftrightarrow \forall z \in (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\}) z \leq 0)$
42	40 37 41	sylancl	$⊢ (φ \land (f \in B \land g \in B)) \to (sup (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} ℝ^{*} <) \leq 0 \leftrightarrow \forall z \in (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\}) z \leq 0)$
43		0le0	$⊢ 0 \leq 0$
44		c0ex	$⊢ 0 \in V$
45		breq1	$⊢ z = 0 \to (z \leq 0 \leftrightarrow 0 \leq 0)$
46	44 45	ralsn	$⊢ \forall z \in \{0\} z \leq 0 \leftrightarrow 0 \leq 0$
47	43 46	mpbir	$⊢ \forall z \in \{0\} z \leq 0$
48		ralunb	$⊢ \forall z \in (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\}) z \leq 0 \leftrightarrow (\forall z \in ran (x \in I ⟼ f (x) E g (x)) z \leq 0 \land \forall z \in \{0\} z \leq 0)$
49	47 48	mpbiran2	$⊢ \forall z \in (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\}) z \leq 0 \leftrightarrow \forall z \in ran (x \in I ⟼ f (x) E g (x)) z \leq 0$
50		ovex	$⊢ f (x) E g (x) \in V$
51	50	rgenw	$⊢ \forall x \in I f (x) E g (x) \in V$
52		eqid	$⊢ (x \in I ⟼ f (x) E g (x)) = (x \in I ⟼ f (x) E g (x))$
53		breq1	$⊢ z = f (x) E g (x) \to (z \leq 0 \leftrightarrow f (x) E g (x) \leq 0)$
54	52 53	ralrnmptw	$⊢ \forall x \in I f (x) E g (x) \in V \to (\forall z \in ran (x \in I ⟼ f (x) E g (x)) z \leq 0 \leftrightarrow \forall x \in I f (x) E g (x) \leq 0)$
55	51 54	ax-mp	$⊢ \forall z \in ran (x \in I ⟼ f (x) E g (x)) z \leq 0 \leftrightarrow \forall x \in I f (x) E g (x) \leq 0$
56	49 55	bitri	$⊢ \forall z \in (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\}) z \leq 0 \leftrightarrow \forall x \in I f (x) E g (x) \leq 0$
57		xmetge0	$⊢ (E \in ∞Met (V) \land f (x) \in V \land g (x) \in V) \to 0 \leq f (x) E g (x)$
58	28 30 32 57	syl3anc	$⊢ ((φ \land (f \in B \land g \in B)) \land x \in I) \to 0 \leq f (x) E g (x)$
59	58	biantrud	$⊢ ((φ \land (f \in B \land g \in B)) \land x \in I) \to (f (x) E g (x) \leq 0 \leftrightarrow (f (x) E g (x) \leq 0 \land 0 \leq f (x) E g (x)))$
60		xrletri3	$⊢ (f (x) E g (x) \in ℝ^{} \land 0 \in ℝ^{}) \to (f (x) E g (x) = 0 \leftrightarrow (f (x) E g (x) \leq 0 \land 0 \leq f (x) E g (x)))$
61	34 37 60	sylancl	$⊢ ((φ \land (f \in B \land g \in B)) \land x \in I) \to (f (x) E g (x) = 0 \leftrightarrow (f (x) E g (x) \leq 0 \land 0 \leq f (x) E g (x)))$
62		xmeteq0	$⊢ (E \in ∞Met (V) \land f (x) \in V \land g (x) \in V) \to (f (x) E g (x) = 0 \leftrightarrow f (x) = g (x))$
63	28 30 32 62	syl3anc	$⊢ ((φ \land (f \in B \land g \in B)) \land x \in I) \to (f (x) E g (x) = 0 \leftrightarrow f (x) = g (x))$
64	59 61 63	3bitr2d	$⊢ ((φ \land (f \in B \land g \in B)) \land x \in I) \to (f (x) E g (x) \leq 0 \leftrightarrow f (x) = g (x))$
65	64	ralbidva	$⊢ (φ \land (f \in B \land g \in B)) \to (\forall x \in I f (x) E g (x) \leq 0 \leftrightarrow \forall x \in I f (x) = g (x))$
66		eqid	$⊢ (x \in I ⟼ R) = (x \in I ⟼ R)$
67	66	fnmpt	$⊢ \forall x \in I R \in Z \to (x \in I ⟼ R) Fn I$
68	22 67	syl	$⊢ φ \to (x \in I ⟼ R) Fn I$
69	68	adantr	$⊢ (φ \land (f \in B \land g \in B)) \to (x \in I ⟼ R) Fn I$
70	1 2 20 21 69 24	prdsbasfn	$⊢ (φ \land (f \in B \land g \in B)) \to f Fn I$
71	1 2 20 21 69 25	prdsbasfn	$⊢ (φ \land (f \in B \land g \in B)) \to g Fn I$
72		eqfnfv	$⊢ (f Fn I \land g Fn I) \to (f = g \leftrightarrow \forall x \in I f (x) = g (x))$
73	70 71 72	syl2anc	$⊢ (φ \land (f \in B \land g \in B)) \to (f = g \leftrightarrow \forall x \in I f (x) = g (x))$
74	65 73	bitr4d	$⊢ (φ \land (f \in B \land g \in B)) \to (\forall x \in I f (x) E g (x) \leq 0 \leftrightarrow f = g)$
75	56 74	syl5bb	$⊢ (φ \land (f \in B \land g \in B)) \to (\forall z \in (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\}) z \leq 0 \leftrightarrow f = g)$
76	27 42 75	3bitrd	$⊢ (φ \land (f \in B \land g \in B)) \to (f D g \leq 0 \leftrightarrow f = g)$
77	26	3adantr3	$⊢ (φ \land (f \in B \land g \in B \land h \in B)) \to f D g = sup (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} ℝ^{*} <)$
78	77	3adant3	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to f D g = sup (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} ℝ^{*} <)$
79	9	3ad2antl1	$⊢ ((φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \land x \in I) \to E \in ∞Met (V)$
80	29	3adantr3	$⊢ (φ \land (f \in B \land g \in B \land h \in B)) \to \forall x \in I f (x) \in V$
81	80	3adant3	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to \forall x \in I f (x) \in V$
82	81	r19.21bi	$⊢ ((φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \land x \in I) \to f (x) \in V$
83	31	3adantr3	$⊢ (φ \land (f \in B \land g \in B \land h \in B)) \to \forall x \in I g (x) \in V$
84	83	3adant3	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to \forall x \in I g (x) \in V$
85	84	r19.21bi	$⊢ ((φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \land x \in I) \to g (x) \in V$
86	79 82 85 33	syl3anc	$⊢ ((φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \land x \in I) \to f (x) E g (x) \in ℝ^{*}$
87	6	3ad2ant1	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to S \in W$
88	7	3ad2ant1	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to I \in X$
89	22	3ad2ant1	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to \forall x \in I R \in Z$
90		simp23	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to h \in B$
91	1 2 87 88 89 3 90	prdsbascl	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to \forall x \in I h (x) \in V$
92	91	r19.21bi	$⊢ ((φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \land x \in I) \to h (x) \in V$
93		xmetcl	$⊢ (E \in ∞Met (V) \land h (x) \in V \land f (x) \in V) \to h (x) E f (x) \in ℝ^{*}$
94	79 92 82 93	syl3anc	$⊢ ((φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \land x \in I) \to h (x) E f (x) \in ℝ^{*}$
95		simp3l	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to h D f \in ℝ$
96	95	adantr	$⊢ ((φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \land x \in I) \to h D f \in ℝ$
97		xmetge0	$⊢ (E \in ∞Met (V) \land h (x) \in V \land f (x) \in V) \to 0 \leq h (x) E f (x)$
98	79 92 82 97	syl3anc	$⊢ ((φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \land x \in I) \to 0 \leq h (x) E f (x)$
99	94	fmpttd	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to (x \in I ⟼ h (x) E f (x)) : I ⟶ ℝ^{*}$
100	99	frnd	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to ran (x \in I ⟼ h (x) E f (x)) \subseteq ℝ^{*}$
101	37	a1i	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to 0 \in ℝ^{*}$
102	101	snssd	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to \{0\} \subseteq ℝ^{*}$
103	100 102	unssd	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to ran (x \in I ⟼ h (x) E f (x)) \cup \{0\} \subseteq ℝ^{*}$
104		ssun1	$⊢ ran (x \in I ⟼ h (x) E f (x)) \subseteq ran (x \in I ⟼ h (x) E f (x)) \cup \{0\}$
105		ovex	$⊢ h (x) E f (x) \in V$
106	105	elabrex	$⊢ x \in I \to h (x) E f (x) \in \{z \| \exists x \in I z = h (x) E f (x)\}$
107	106	adantl	$⊢ ((φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \land x \in I) \to h (x) E f (x) \in \{z \| \exists x \in I z = h (x) E f (x)\}$
108		eqid	$⊢ (x \in I ⟼ h (x) E f (x)) = (x \in I ⟼ h (x) E f (x))$
109	108	rnmpt	$⊢ ran (x \in I ⟼ h (x) E f (x)) = \{z \| \exists x \in I z = h (x) E f (x)\}$
110	107 109	eleqtrrdi	$⊢ ((φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \land x \in I) \to h (x) E f (x) \in ran (x \in I ⟼ h (x) E f (x))$
111	104 110	sselid	$⊢ ((φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \land x \in I) \to h (x) E f (x) \in (ran (x \in I ⟼ h (x) E f (x)) \cup \{0\})$
112		supxrub	$⊢ (ran (x \in I ⟼ h (x) E f (x)) \cup \{0\} \subseteq ℝ^{} \land h (x) E f (x) \in (ran (x \in I ⟼ h (x) E f (x)) \cup \{0\})) \to h (x) E f (x) \leq sup (ran (x \in I ⟼ h (x) E f (x)) \cup \{0\} ℝ^{} <)$
113	103 111 112	syl2an2r	$⊢ ((φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \land x \in I) \to h (x) E f (x) \leq sup (ran (x \in I ⟼ h (x) E f (x)) \cup \{0\} ℝ^{*} <)$
114		simp21	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to f \in B$
115	1 2 87 88 89 90 114 3 4 5	prdsdsval3	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to h D f = sup (ran (x \in I ⟼ h (x) E f (x)) \cup \{0\} ℝ^{*} <)$
116	115	adantr	$⊢ ((φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \land x \in I) \to h D f = sup (ran (x \in I ⟼ h (x) E f (x)) \cup \{0\} ℝ^{*} <)$
117	113 116	breqtrrd	$⊢ ((φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \land x \in I) \to h (x) E f (x) \leq h D f$
118		xrrege0	$⊢ ((h (x) E f (x) \in ℝ^{*} \land h D f \in ℝ) \land (0 \leq h (x) E f (x) \land h (x) E f (x) \leq h D f)) \to h (x) E f (x) \in ℝ$
119	94 96 98 117 118	syl22anc	$⊢ ((φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \land x \in I) \to h (x) E f (x) \in ℝ$
120		xmetcl	$⊢ (E \in ∞Met (V) \land h (x) \in V \land g (x) \in V) \to h (x) E g (x) \in ℝ^{*}$
121	79 92 85 120	syl3anc	$⊢ ((φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \land x \in I) \to h (x) E g (x) \in ℝ^{*}$
122		simp3r	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to h D g \in ℝ$
123	122	adantr	$⊢ ((φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \land x \in I) \to h D g \in ℝ$
124		xmetge0	$⊢ (E \in ∞Met (V) \land h (x) \in V \land g (x) \in V) \to 0 \leq h (x) E g (x)$
125	79 92 85 124	syl3anc	$⊢ ((φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \land x \in I) \to 0 \leq h (x) E g (x)$
126	121	fmpttd	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to (x \in I ⟼ h (x) E g (x)) : I ⟶ ℝ^{*}$
127	126	frnd	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to ran (x \in I ⟼ h (x) E g (x)) \subseteq ℝ^{*}$
128	127 102	unssd	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to ran (x \in I ⟼ h (x) E g (x)) \cup \{0\} \subseteq ℝ^{*}$
129		ssun1	$⊢ ran (x \in I ⟼ h (x) E g (x)) \subseteq ran (x \in I ⟼ h (x) E g (x)) \cup \{0\}$
130		ovex	$⊢ h (x) E g (x) \in V$
131	130	elabrex	$⊢ x \in I \to h (x) E g (x) \in \{z \| \exists x \in I z = h (x) E g (x)\}$
132	131	adantl	$⊢ ((φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \land x \in I) \to h (x) E g (x) \in \{z \| \exists x \in I z = h (x) E g (x)\}$
133		eqid	$⊢ (x \in I ⟼ h (x) E g (x)) = (x \in I ⟼ h (x) E g (x))$
134	133	rnmpt	$⊢ ran (x \in I ⟼ h (x) E g (x)) = \{z \| \exists x \in I z = h (x) E g (x)\}$
135	132 134	eleqtrrdi	$⊢ ((φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \land x \in I) \to h (x) E g (x) \in ran (x \in I ⟼ h (x) E g (x))$
136	129 135	sselid	$⊢ ((φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \land x \in I) \to h (x) E g (x) \in (ran (x \in I ⟼ h (x) E g (x)) \cup \{0\})$
137		supxrub	$⊢ (ran (x \in I ⟼ h (x) E g (x)) \cup \{0\} \subseteq ℝ^{} \land h (x) E g (x) \in (ran (x \in I ⟼ h (x) E g (x)) \cup \{0\})) \to h (x) E g (x) \leq sup (ran (x \in I ⟼ h (x) E g (x)) \cup \{0\} ℝ^{} <)$
138	128 136 137	syl2an2r	$⊢ ((φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \land x \in I) \to h (x) E g (x) \leq sup (ran (x \in I ⟼ h (x) E g (x)) \cup \{0\} ℝ^{*} <)$
139		simp22	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to g \in B$
140	1 2 87 88 89 90 139 3 4 5	prdsdsval3	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to h D g = sup (ran (x \in I ⟼ h (x) E g (x)) \cup \{0\} ℝ^{*} <)$
141	140	adantr	$⊢ ((φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \land x \in I) \to h D g = sup (ran (x \in I ⟼ h (x) E g (x)) \cup \{0\} ℝ^{*} <)$
142	138 141	breqtrrd	$⊢ ((φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \land x \in I) \to h (x) E g (x) \leq h D g$
143		xrrege0	$⊢ ((h (x) E g (x) \in ℝ^{*} \land h D g \in ℝ) \land (0 \leq h (x) E g (x) \land h (x) E g (x) \leq h D g)) \to h (x) E g (x) \in ℝ$
144	121 123 125 142 143	syl22anc	$⊢ ((φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \land x \in I) \to h (x) E g (x) \in ℝ$
145	119 144	readdcld	$⊢ ((φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \land x \in I) \to (h (x) E f (x)) + (h (x) E g (x)) \in ℝ$
146	79 82 85 57	syl3anc	$⊢ ((φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \land x \in I) \to 0 \leq f (x) E g (x)$
147		xmettri2	$⊢ (E \in ∞Met (V) \land (h (x) \in V \land f (x) \in V \land g (x) \in V)) \to f (x) E g (x) \leq (h (x) E f (x)) +_{𝑒} (h (x) E g (x))$
148	79 92 82 85 147	syl13anc	$⊢ ((φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \land x \in I) \to f (x) E g (x) \leq (h (x) E f (x)) +_{𝑒} (h (x) E g (x))$
149	119 144	rexaddd	$⊢ ((φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \land x \in I) \to (h (x) E f (x)) +_{𝑒} (h (x) E g (x)) = (h (x) E f (x)) + (h (x) E g (x))$
150	148 149	breqtrd	$⊢ ((φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \land x \in I) \to f (x) E g (x) \leq (h (x) E f (x)) + (h (x) E g (x))$
151		xrrege0	$⊢ ((f (x) E g (x) \in ℝ^{*} \land (h (x) E f (x)) + (h (x) E g (x)) \in ℝ) \land (0 \leq f (x) E g (x) \land f (x) E g (x) \leq (h (x) E f (x)) + (h (x) E g (x)))) \to f (x) E g (x) \in ℝ$
152	86 145 146 150 151	syl22anc	$⊢ ((φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \land x \in I) \to f (x) E g (x) \in ℝ$
153		readdcl	$⊢ (h D f \in ℝ \land h D g \in ℝ) \to (h D f) + (h D g) \in ℝ$
154	153	3ad2ant3	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to (h D f) + (h D g) \in ℝ$
155	154	adantr	$⊢ ((φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \land x \in I) \to (h D f) + (h D g) \in ℝ$
156	119 144 96 123 117 142	le2addd	$⊢ ((φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \land x \in I) \to (h (x) E f (x)) + (h (x) E g (x)) \leq (h D f) + (h D g)$
157	152 145 155 150 156	letrd	$⊢ ((φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \land x \in I) \to f (x) E g (x) \leq (h D f) + (h D g)$
158	157	ralrimiva	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to \forall x \in I f (x) E g (x) \leq (h D f) + (h D g)$
159	86	ralrimiva	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to \forall x \in I f (x) E g (x) \in ℝ^{*}$
160		breq1	$⊢ z = f (x) E g (x) \to (z \leq (h D f) + (h D g) \leftrightarrow f (x) E g (x) \leq (h D f) + (h D g))$
161	52 160	ralrnmptw	$⊢ \forall x \in I f (x) E g (x) \in ℝ^{*} \to (\forall z \in ran (x \in I ⟼ f (x) E g (x)) z \leq (h D f) + (h D g) \leftrightarrow \forall x \in I f (x) E g (x) \leq (h D f) + (h D g))$
162	159 161	syl	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to (\forall z \in ran (x \in I ⟼ f (x) E g (x)) z \leq (h D f) + (h D g) \leftrightarrow \forall x \in I f (x) E g (x) \leq (h D f) + (h D g))$
163	158 162	mpbird	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to \forall z \in ran (x \in I ⟼ f (x) E g (x)) z \leq (h D f) + (h D g)$
164	12	3ad2ant1	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to D : B \times B ⟶ [0, +∞]$
165	164 90 114	fovrnd	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to h D f \in [0, +∞]$
166		elxrge0	$⊢ h D f \in [0, +∞] \leftrightarrow (h D f \in ℝ^{*} \land 0 \leq h D f)$
167	166	simprbi	$⊢ h D f \in [0, +∞] \to 0 \leq h D f$
168	165 167	syl	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to 0 \leq h D f$
169	164 90 139	fovrnd	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to h D g \in [0, +∞]$
170		elxrge0	$⊢ h D g \in [0, +∞] \leftrightarrow (h D g \in ℝ^{*} \land 0 \leq h D g)$
171	170	simprbi	$⊢ h D g \in [0, +∞] \to 0 \leq h D g$
172	169 171	syl	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to 0 \leq h D g$
173	95 122 168 172	addge0d	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to 0 \leq (h D f) + (h D g)$
174		breq1	$⊢ z = 0 \to (z \leq (h D f) + (h D g) \leftrightarrow 0 \leq (h D f) + (h D g))$
175	44 174	ralsn	$⊢ \forall z \in \{0\} z \leq (h D f) + (h D g) \leftrightarrow 0 \leq (h D f) + (h D g)$
176	173 175	sylibr	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to \forall z \in \{0\} z \leq (h D f) + (h D g)$
177		ralunb	$⊢ \forall z \in (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\}) z \leq (h D f) + (h D g) \leftrightarrow (\forall z \in ran (x \in I ⟼ f (x) E g (x)) z \leq (h D f) + (h D g) \land \forall z \in \{0\} z \leq (h D f) + (h D g))$
178	163 176 177	sylanbrc	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to \forall z \in (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\}) z \leq (h D f) + (h D g)$
179	40	3adantr3	$⊢ (φ \land (f \in B \land g \in B \land h \in B)) \to ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} \subseteq ℝ^{*}$
180	179	3adant3	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} \subseteq ℝ^{*}$
181	154	rexrd	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to (h D f) + (h D g) \in ℝ^{*}$
182		supxrleub	$⊢ (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} \subseteq ℝ^{} \land (h D f) + (h D g) \in ℝ^{}) \to (sup (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} ℝ^{*} <) \leq (h D f) + (h D g) \leftrightarrow \forall z \in (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\}) z \leq (h D f) + (h D g))$
183	180 181 182	syl2anc	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to (sup (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} ℝ^{*} <) \leq (h D f) + (h D g) \leftrightarrow \forall z \in (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\}) z \leq (h D f) + (h D g))$
184	178 183	mpbird	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to sup (ran (x \in I ⟼ f (x) E g (x)) \cup \{0\} ℝ^{*} <) \leq (h D f) + (h D g)$
185	78 184	eqbrtrd	$⊢ (φ \land (f \in B \land g \in B \land h \in B) \land (h D f \in ℝ \land h D g \in ℝ)) \to f D g \leq (h D f) + (h D g)$
186	11 15 19 76 185	isxmet2d	$⊢ φ \to D \in ∞Met (B)$

Metamath Proof Explorer

Theorem prdsxmetlem

Proof