comet

Description: The composition of an extended metric with a monotonic subadditive function is an extended metric. (Contributed by Mario Carneiro, 21-Mar-2015)

	Ref	Expression
Hypotheses	comet.1	$⊢ φ \to D \in ∞Met (X)$
	comet.2	$⊢ φ \to F : [0, +∞] ⟶ ℝ^{*}$
	comet.3	$⊢ (φ \land x \in [0, +∞]) \to (F (x) = 0 \leftrightarrow x = 0)$
	comet.4	$⊢ (φ \land (x \in [0, +∞] \land y \in [0, +∞])) \to (x \leq y \to F (x) \leq F (y))$
	comet.5	$⊢ (φ \land (x \in [0, +∞] \land y \in [0, +∞])) \to F (x +_{𝑒} y) \leq F (x) +_{𝑒} F (y)$
Assertion	comet	$⊢ φ \to F \circ D \in ∞Met (X)$

Proof

Step	Hyp	Ref	Expression
1		comet.1	$⊢ φ \to D \in ∞Met (X)$
2		comet.2	$⊢ φ \to F : [0, +∞] ⟶ ℝ^{*}$
3		comet.3	$⊢ (φ \land x \in [0, +∞]) \to (F (x) = 0 \leftrightarrow x = 0)$
4		comet.4	$⊢ (φ \land (x \in [0, +∞] \land y \in [0, +∞])) \to (x \leq y \to F (x) \leq F (y))$
5		comet.5	$⊢ (φ \land (x \in [0, +∞] \land y \in [0, +∞])) \to F (x +_{𝑒} y) \leq F (x) +_{𝑒} F (y)$
6	1	elfvexd	$⊢ φ \to X \in V$
7		xmetf	$⊢ D \in ∞Met (X) \to D : X \times X ⟶ ℝ^{*}$
8	1 7	syl	$⊢ φ \to D : X \times X ⟶ ℝ^{*}$
9	8	ffnd	$⊢ φ \to D Fn (X \times X)$
10		xmetcl	$⊢ (D \in ∞Met (X) \land a \in X \land b \in X) \to a D b \in ℝ^{*}$
11		xmetge0	$⊢ (D \in ∞Met (X) \land a \in X \land b \in X) \to 0 \leq a D b$
12		elxrge0	$⊢ a D b \in [0, +∞] \leftrightarrow (a D b \in ℝ^{*} \land 0 \leq a D b)$
13	10 11 12	sylanbrc	$⊢ (D \in ∞Met (X) \land a \in X \land b \in X) \to a D b \in [0, +∞]$
14	13	3expb	$⊢ (D \in ∞Met (X) \land (a \in X \land b \in X)) \to a D b \in [0, +∞]$
15	1 14	sylan	$⊢ (φ \land (a \in X \land b \in X)) \to a D b \in [0, +∞]$
16	15	ralrimivva	$⊢ φ \to \forall a \in X \forall b \in X a D b \in [0, +∞]$
17		ffnov	$⊢ D : X \times X ⟶ [0, +∞] \leftrightarrow (D Fn (X \times X) \land \forall a \in X \forall b \in X a D b \in [0, +∞])$
18	9 16 17	sylanbrc	$⊢ φ \to D : X \times X ⟶ [0, +∞]$
19	2 18	fcod	$⊢ φ \to (F \circ D) : X \times X ⟶ ℝ^{*}$
20		opelxpi	$⊢ (a \in X \land b \in X) \to ⟨a, b⟩ \in (X \times X)$
21		fvco3	$⊢ (D : X \times X ⟶ ℝ^{*} \land ⟨a, b⟩ \in (X \times X)) \to (F \circ D) (⟨a, b⟩) = F (D (⟨a, b⟩))$
22	8 20 21	syl2an	$⊢ (φ \land (a \in X \land b \in X)) \to (F \circ D) (⟨a, b⟩) = F (D (⟨a, b⟩))$
23		df-ov	$⊢ a (F \circ D) b = (F \circ D) (⟨a, b⟩)$
24		df-ov	$⊢ a D b = D (⟨a, b⟩)$
25	24	fveq2i	$⊢ F (a D b) = F (D (⟨a, b⟩))$
26	22 23 25	3eqtr4g	$⊢ (φ \land (a \in X \land b \in X)) \to a (F \circ D) b = F (a D b)$
27	26	eqeq1d	$⊢ (φ \land (a \in X \land b \in X)) \to (a (F \circ D) b = 0 \leftrightarrow F (a D b) = 0)$
28		fveq2	$⊢ x = a D b \to F (x) = F (a D b)$
29	28	eqeq1d	$⊢ x = a D b \to (F (x) = 0 \leftrightarrow F (a D b) = 0)$
30		eqeq1	$⊢ x = a D b \to (x = 0 \leftrightarrow a D b = 0)$
31	29 30	bibi12d	$⊢ x = a D b \to ((F (x) = 0 \leftrightarrow x = 0) \leftrightarrow (F (a D b) = 0 \leftrightarrow a D b = 0))$
32	3	ralrimiva	$⊢ φ \to \forall x \in [0, +∞] (F (x) = 0 \leftrightarrow x = 0)$
33	32	adantr	$⊢ (φ \land (a \in X \land b \in X)) \to \forall x \in [0, +∞] (F (x) = 0 \leftrightarrow x = 0)$
34	31 33 15	rspcdva	$⊢ (φ \land (a \in X \land b \in X)) \to (F (a D b) = 0 \leftrightarrow a D b = 0)$
35		xmeteq0	$⊢ (D \in ∞Met (X) \land a \in X \land b \in X) \to (a D b = 0 \leftrightarrow a = b)$
36	35	3expb	$⊢ (D \in ∞Met (X) \land (a \in X \land b \in X)) \to (a D b = 0 \leftrightarrow a = b)$
37	1 36	sylan	$⊢ (φ \land (a \in X \land b \in X)) \to (a D b = 0 \leftrightarrow a = b)$
38	27 34 37	3bitrd	$⊢ (φ \land (a \in X \land b \in X)) \to (a (F \circ D) b = 0 \leftrightarrow a = b)$
39	2	adantr	$⊢ (φ \land (a \in X \land b \in X \land c \in X)) \to F : [0, +∞] ⟶ ℝ^{*}$
40	15	3adantr3	$⊢ (φ \land (a \in X \land b \in X \land c \in X)) \to a D b \in [0, +∞]$
41	39 40	ffvelrnd	$⊢ (φ \land (a \in X \land b \in X \land c \in X)) \to F (a D b) \in ℝ^{*}$
42	18	adantr	$⊢ (φ \land (a \in X \land b \in X \land c \in X)) \to D : X \times X ⟶ [0, +∞]$
43		simpr3	$⊢ (φ \land (a \in X \land b \in X \land c \in X)) \to c \in X$
44		simpr1	$⊢ (φ \land (a \in X \land b \in X \land c \in X)) \to a \in X$
45	42 43 44	fovrnd	$⊢ (φ \land (a \in X \land b \in X \land c \in X)) \to c D a \in [0, +∞]$
46		simpr2	$⊢ (φ \land (a \in X \land b \in X \land c \in X)) \to b \in X$
47	42 43 46	fovrnd	$⊢ (φ \land (a \in X \land b \in X \land c \in X)) \to c D b \in [0, +∞]$
48		ge0xaddcl	$⊢ (c D a \in [0, +∞] \land c D b \in [0, +∞]) \to (c D a) +_{𝑒} (c D b) \in [0, +∞]$
49	45 47 48	syl2anc	$⊢ (φ \land (a \in X \land b \in X \land c \in X)) \to (c D a) +_{𝑒} (c D b) \in [0, +∞]$
50	39 49	ffvelrnd	$⊢ (φ \land (a \in X \land b \in X \land c \in X)) \to F ((c D a) +_{𝑒} (c D b)) \in ℝ^{*}$
51	39 45	ffvelrnd	$⊢ (φ \land (a \in X \land b \in X \land c \in X)) \to F (c D a) \in ℝ^{*}$
52	39 47	ffvelrnd	$⊢ (φ \land (a \in X \land b \in X \land c \in X)) \to F (c D b) \in ℝ^{*}$
53	51 52	xaddcld	$⊢ (φ \land (a \in X \land b \in X \land c \in X)) \to F (c D a) +_{𝑒} F (c D b) \in ℝ^{*}$
54		3anrot	$⊢ (c \in X \land a \in X \land b \in X) \leftrightarrow (a \in X \land b \in X \land c \in X)$
55		xmettri2	$⊢ (D \in ∞Met (X) \land (c \in X \land a \in X \land b \in X)) \to a D b \leq (c D a) +_{𝑒} (c D b)$
56	54 55	sylan2br	$⊢ (D \in ∞Met (X) \land (a \in X \land b \in X \land c \in X)) \to a D b \leq (c D a) +_{𝑒} (c D b)$
57	1 56	sylan	$⊢ (φ \land (a \in X \land b \in X \land c \in X)) \to a D b \leq (c D a) +_{𝑒} (c D b)$
58	4	ralrimivva	$⊢ φ \to \forall x \in [0, +∞] \forall y \in [0, +∞] (x \leq y \to F (x) \leq F (y))$
59	58	adantr	$⊢ (φ \land (a \in X \land b \in X \land c \in X)) \to \forall x \in [0, +∞] \forall y \in [0, +∞] (x \leq y \to F (x) \leq F (y))$
60		breq1	$⊢ x = a D b \to (x \leq y \leftrightarrow a D b \leq y)$
61	28	breq1d	$⊢ x = a D b \to (F (x) \leq F (y) \leftrightarrow F (a D b) \leq F (y))$
62	60 61	imbi12d	$⊢ x = a D b \to ((x \leq y \to F (x) \leq F (y)) \leftrightarrow (a D b \leq y \to F (a D b) \leq F (y)))$
63		breq2	$⊢ y = (c D a) +_{𝑒} (c D b) \to (a D b \leq y \leftrightarrow a D b \leq (c D a) +_{𝑒} (c D b))$
64		fveq2	$⊢ y = (c D a) +_{𝑒} (c D b) \to F (y) = F ((c D a) +_{𝑒} (c D b))$
65	64	breq2d	$⊢ y = (c D a) +_{𝑒} (c D b) \to (F (a D b) \leq F (y) \leftrightarrow F (a D b) \leq F ((c D a) +_{𝑒} (c D b)))$
66	63 65	imbi12d	$⊢ y = (c D a) +_{𝑒} (c D b) \to ((a D b \leq y \to F (a D b) \leq F (y)) \leftrightarrow (a D b \leq (c D a) +_{𝑒} (c D b) \to F (a D b) \leq F ((c D a) +_{𝑒} (c D b))))$
67	62 66	rspc2va	$⊢ ((a D b \in [0, +∞] \land (c D a) +_{𝑒} (c D b) \in [0, +∞]) \land \forall x \in [0, +∞] \forall y \in [0, +∞] (x \leq y \to F (x) \leq F (y))) \to (a D b \leq (c D a) +_{𝑒} (c D b) \to F (a D b) \leq F ((c D a) +_{𝑒} (c D b)))$
68	40 49 59 67	syl21anc	$⊢ (φ \land (a \in X \land b \in X \land c \in X)) \to (a D b \leq (c D a) +_{𝑒} (c D b) \to F (a D b) \leq F ((c D a) +_{𝑒} (c D b)))$
69	57 68	mpd	$⊢ (φ \land (a \in X \land b \in X \land c \in X)) \to F (a D b) \leq F ((c D a) +_{𝑒} (c D b))$
70	5	ralrimivva	$⊢ φ \to \forall x \in [0, +∞] \forall y \in [0, +∞] F (x +_{𝑒} y) \leq F (x) +_{𝑒} F (y)$
71	70	adantr	$⊢ (φ \land (a \in X \land b \in X \land c \in X)) \to \forall x \in [0, +∞] \forall y \in [0, +∞] F (x +_{𝑒} y) \leq F (x) +_{𝑒} F (y)$
72		fvoveq1	$⊢ x = c D a \to F (x +_{𝑒} y) = F ((c D a) +_{𝑒} y)$
73		fveq2	$⊢ x = c D a \to F (x) = F (c D a)$
74	73	oveq1d	$⊢ x = c D a \to F (x) +_{𝑒} F (y) = F (c D a) +_{𝑒} F (y)$
75	72 74	breq12d	$⊢ x = c D a \to (F (x +_{𝑒} y) \leq F (x) +_{𝑒} F (y) \leftrightarrow F ((c D a) +_{𝑒} y) \leq F (c D a) +_{𝑒} F (y))$
76		oveq2	$⊢ y = c D b \to (c D a) +_{𝑒} y = (c D a) +_{𝑒} (c D b)$
77	76	fveq2d	$⊢ y = c D b \to F ((c D a) +_{𝑒} y) = F ((c D a) +_{𝑒} (c D b))$
78		fveq2	$⊢ y = c D b \to F (y) = F (c D b)$
79	78	oveq2d	$⊢ y = c D b \to F (c D a) +_{𝑒} F (y) = F (c D a) +_{𝑒} F (c D b)$
80	77 79	breq12d	$⊢ y = c D b \to (F ((c D a) +_{𝑒} y) \leq F (c D a) +_{𝑒} F (y) \leftrightarrow F ((c D a) +_{𝑒} (c D b)) \leq F (c D a) +_{𝑒} F (c D b))$
81	75 80	rspc2va	$⊢ ((c D a \in [0, +∞] \land c D b \in [0, +∞]) \land \forall x \in [0, +∞] \forall y \in [0, +∞] F (x +_{𝑒} y) \leq F (x) +_{𝑒} F (y)) \to F ((c D a) +_{𝑒} (c D b)) \leq F (c D a) +_{𝑒} F (c D b)$
82	45 47 71 81	syl21anc	$⊢ (φ \land (a \in X \land b \in X \land c \in X)) \to F ((c D a) +_{𝑒} (c D b)) \leq F (c D a) +_{𝑒} F (c D b)$
83	41 50 53 69 82	xrletrd	$⊢ (φ \land (a \in X \land b \in X \land c \in X)) \to F (a D b) \leq F (c D a) +_{𝑒} F (c D b)$
84	26	3adantr3	$⊢ (φ \land (a \in X \land b \in X \land c \in X)) \to a (F \circ D) b = F (a D b)$
85	8	adantr	$⊢ (φ \land (a \in X \land b \in X \land c \in X)) \to D : X \times X ⟶ ℝ^{*}$
86	43 44	opelxpd	$⊢ (φ \land (a \in X \land b \in X \land c \in X)) \to ⟨c, a⟩ \in (X \times X)$
87	85 86	fvco3d	$⊢ (φ \land (a \in X \land b \in X \land c \in X)) \to (F \circ D) (⟨c, a⟩) = F (D (⟨c, a⟩))$
88		df-ov	$⊢ c (F \circ D) a = (F \circ D) (⟨c, a⟩)$
89		df-ov	$⊢ c D a = D (⟨c, a⟩)$
90	89	fveq2i	$⊢ F (c D a) = F (D (⟨c, a⟩))$
91	87 88 90	3eqtr4g	$⊢ (φ \land (a \in X \land b \in X \land c \in X)) \to c (F \circ D) a = F (c D a)$
92	43 46	opelxpd	$⊢ (φ \land (a \in X \land b \in X \land c \in X)) \to ⟨c, b⟩ \in (X \times X)$
93	85 92	fvco3d	$⊢ (φ \land (a \in X \land b \in X \land c \in X)) \to (F \circ D) (⟨c, b⟩) = F (D (⟨c, b⟩))$
94		df-ov	$⊢ c (F \circ D) b = (F \circ D) (⟨c, b⟩)$
95		df-ov	$⊢ c D b = D (⟨c, b⟩)$
96	95	fveq2i	$⊢ F (c D b) = F (D (⟨c, b⟩))$
97	93 94 96	3eqtr4g	$⊢ (φ \land (a \in X \land b \in X \land c \in X)) \to c (F \circ D) b = F (c D b)$
98	91 97	oveq12d	$⊢ (φ \land (a \in X \land b \in X \land c \in X)) \to (c (F \circ D) a) +_{𝑒} (c (F \circ D) b) = F (c D a) +_{𝑒} F (c D b)$
99	83 84 98	3brtr4d	$⊢ (φ \land (a \in X \land b \in X \land c \in X)) \to a (F \circ D) b \leq (c (F \circ D) a) +_{𝑒} (c (F \circ D) b)$
100	6 19 38 99	isxmetd	$⊢ φ \to F \circ D \in ∞Met (X)$

Metamath Proof Explorer

Theorem comet

Proof