Theorem 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	⊢ ( 𝜑 → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
	comet.2	⊢ ( 𝜑 → 𝐹 : ( 0 [,] +∞ ) ⟶ ℝ* )
	comet.3	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 0 [,] +∞ ) ) → ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = 0 ) )
	comet.4	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ) → ( 𝑥 ≤ 𝑦 → ( 𝐹 ‘ 𝑥 ) ≤ ( 𝐹 ‘ 𝑦 ) ) )
	comet.5	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 0 [,] +∞ ) ∧ 𝑦 ∈ ( 0 [,] +∞ ) ) ) → ( 𝐹 ‘ ( 𝑥 +𝑒 𝑦 ) ) ≤ ( ( 𝐹 ‘ 𝑥 ) +𝑒 ( 𝐹 ‘ 𝑦 ) ) )
Assertion	comet	⊢ ( 𝜑 → ( 𝐹 ∘ 𝐷 ) ∈ ( ∞Met ‘ 𝑋 ) )

Proof

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