Metamath Proof Explorer

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 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑎 𝐷 𝑏 ) ) ∈ ℝ* )
42 18 adantr ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ( 0 [,] +∞ ) )
43 simpr3 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → 𝑐 ∈ 𝑋 )
44 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → 𝑎 ∈ 𝑋 )
45 42 43 44 fovrnd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝑐 𝐷 𝑎 ) ∈ ( 0 [,] +∞ ) )
46 simpr2 ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → 𝑏 ∈ 𝑋 )
47 42 43 46 fovrnd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝑐 𝐷 𝑏 ) ∈ ( 0 [,] +∞ ) )
48 ge0xaddcl ⊢ ( ( ( 𝑐 𝐷 𝑎 ) ∈ ( 0 [,] +∞ ) ∧ ( 𝑐 𝐷 𝑏 ) ∈ ( 0 [,] +∞ ) ) → ( ( 𝑐 𝐷 𝑎 ) +𝑒 ( 𝑐 𝐷 𝑏 ) ) ∈ ( 0 [,] +∞ ) )
49 45 47 48 syl2anc ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → ( ( 𝑐 𝐷 𝑎 ) +𝑒 ( 𝑐 𝐷 𝑏 ) ) ∈ ( 0 [,] +∞ ) )
50 39 49 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( ( 𝑐 𝐷 𝑎 ) +𝑒 ( 𝑐 𝐷 𝑏 ) ) ) ∈ ℝ* )
51 39 45 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑐 𝐷 𝑎 ) ) ∈ ℝ* )
52 39 47 ffvelrnd ⊢ ( ( 𝜑 ∧ ( 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑐 𝐷 𝑏 ) ) ∈ ℝ* )
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 ‘ 𝑋 ) )