Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  comet Structured version   Visualization version   GIF version

Theorem comet 22842
 Description: The composition of an extended metric with a monotonic subadditive function is an extended metric. (Contributed by Mario Carneiro, 21-Mar-2015.)
Hypotheses
Ref Expression
comet.1 (𝜑𝐷 ∈ (∞Met‘𝑋))
comet.2 (𝜑𝐹:(0[,]+∞)⟶ℝ*)
comet.3 ((𝜑𝑥 ∈ (0[,]+∞)) → ((𝐹𝑥) = 0 ↔ 𝑥 = 0))
comet.4 ((𝜑 ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞))) → (𝑥𝑦 → (𝐹𝑥) ≤ (𝐹𝑦)))
comet.5 ((𝜑 ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞))) → (𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹𝑥) +𝑒 (𝐹𝑦)))
Assertion
Ref Expression
comet (𝜑 → (𝐹𝐷) ∈ (∞Met‘𝑋))
Distinct variable groups:   𝑥,𝑦,𝐷   𝑥,𝐹,𝑦   𝜑,𝑥,𝑦
Allowed substitution hints:   𝑋(𝑥,𝑦)

Proof of Theorem comet
Dummy variables 𝑎 𝑏 𝑐 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 comet.1 . . 3 (𝜑𝐷 ∈ (∞Met‘𝑋))
21elfvexd 6532 . 2 (𝜑𝑋 ∈ V)
3 comet.2 . . 3 (𝜑𝐹:(0[,]+∞)⟶ℝ*)
4 xmetf 22658 . . . . . 6 (𝐷 ∈ (∞Met‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
51, 4syl 17 . . . . 5 (𝜑𝐷:(𝑋 × 𝑋)⟶ℝ*)
65ffnd 6343 . . . 4 (𝜑𝐷 Fn (𝑋 × 𝑋))
7 xmetcl 22660 . . . . . . . 8 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑎𝑋𝑏𝑋) → (𝑎𝐷𝑏) ∈ ℝ*)
8 xmetge0 22673 . . . . . . . 8 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑎𝑋𝑏𝑋) → 0 ≤ (𝑎𝐷𝑏))
9 elxrge0 12660 . . . . . . . 8 ((𝑎𝐷𝑏) ∈ (0[,]+∞) ↔ ((𝑎𝐷𝑏) ∈ ℝ* ∧ 0 ≤ (𝑎𝐷𝑏)))
107, 8, 9sylanbrc 575 . . . . . . 7 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑎𝑋𝑏𝑋) → (𝑎𝐷𝑏) ∈ (0[,]+∞))
11103expb 1101 . . . . . 6 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑎𝑋𝑏𝑋)) → (𝑎𝐷𝑏) ∈ (0[,]+∞))
121, 11sylan 572 . . . . 5 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → (𝑎𝐷𝑏) ∈ (0[,]+∞))
1312ralrimivva 3136 . . . 4 (𝜑 → ∀𝑎𝑋𝑏𝑋 (𝑎𝐷𝑏) ∈ (0[,]+∞))
14 ffnov 7093 . . . 4 (𝐷:(𝑋 × 𝑋)⟶(0[,]+∞) ↔ (𝐷 Fn (𝑋 × 𝑋) ∧ ∀𝑎𝑋𝑏𝑋 (𝑎𝐷𝑏) ∈ (0[,]+∞)))
156, 13, 14sylanbrc 575 . . 3 (𝜑𝐷:(𝑋 × 𝑋)⟶(0[,]+∞))
16 fco 6359 . . 3 ((𝐹:(0[,]+∞)⟶ℝ*𝐷:(𝑋 × 𝑋)⟶(0[,]+∞)) → (𝐹𝐷):(𝑋 × 𝑋)⟶ℝ*)
173, 15, 16syl2anc 576 . 2 (𝜑 → (𝐹𝐷):(𝑋 × 𝑋)⟶ℝ*)
18 opelxpi 5441 . . . . . 6 ((𝑎𝑋𝑏𝑋) → ⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑋))
19 fvco3 6587 . . . . . 6 ((𝐷:(𝑋 × 𝑋)⟶ℝ* ∧ ⟨𝑎, 𝑏⟩ ∈ (𝑋 × 𝑋)) → ((𝐹𝐷)‘⟨𝑎, 𝑏⟩) = (𝐹‘(𝐷‘⟨𝑎, 𝑏⟩)))
205, 18, 19syl2an 587 . . . . 5 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → ((𝐹𝐷)‘⟨𝑎, 𝑏⟩) = (𝐹‘(𝐷‘⟨𝑎, 𝑏⟩)))
21 df-ov 6978 . . . . 5 (𝑎(𝐹𝐷)𝑏) = ((𝐹𝐷)‘⟨𝑎, 𝑏⟩)
22 df-ov 6978 . . . . . 6 (𝑎𝐷𝑏) = (𝐷‘⟨𝑎, 𝑏⟩)
2322fveq2i 6500 . . . . 5 (𝐹‘(𝑎𝐷𝑏)) = (𝐹‘(𝐷‘⟨𝑎, 𝑏⟩))
2420, 21, 233eqtr4g 2834 . . . 4 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → (𝑎(𝐹𝐷)𝑏) = (𝐹‘(𝑎𝐷𝑏)))
2524eqeq1d 2775 . . 3 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → ((𝑎(𝐹𝐷)𝑏) = 0 ↔ (𝐹‘(𝑎𝐷𝑏)) = 0))
26 fveq2 6497 . . . . . 6 (𝑥 = (𝑎𝐷𝑏) → (𝐹𝑥) = (𝐹‘(𝑎𝐷𝑏)))
2726eqeq1d 2775 . . . . 5 (𝑥 = (𝑎𝐷𝑏) → ((𝐹𝑥) = 0 ↔ (𝐹‘(𝑎𝐷𝑏)) = 0))
28 eqeq1 2777 . . . . 5 (𝑥 = (𝑎𝐷𝑏) → (𝑥 = 0 ↔ (𝑎𝐷𝑏) = 0))
2927, 28bibi12d 338 . . . 4 (𝑥 = (𝑎𝐷𝑏) → (((𝐹𝑥) = 0 ↔ 𝑥 = 0) ↔ ((𝐹‘(𝑎𝐷𝑏)) = 0 ↔ (𝑎𝐷𝑏) = 0)))
30 comet.3 . . . . . 6 ((𝜑𝑥 ∈ (0[,]+∞)) → ((𝐹𝑥) = 0 ↔ 𝑥 = 0))
3130ralrimiva 3127 . . . . 5 (𝜑 → ∀𝑥 ∈ (0[,]+∞)((𝐹𝑥) = 0 ↔ 𝑥 = 0))
3231adantr 473 . . . 4 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → ∀𝑥 ∈ (0[,]+∞)((𝐹𝑥) = 0 ↔ 𝑥 = 0))
3329, 32, 12rspcdva 3536 . . 3 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → ((𝐹‘(𝑎𝐷𝑏)) = 0 ↔ (𝑎𝐷𝑏) = 0))
34 xmeteq0 22667 . . . . 5 ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑎𝑋𝑏𝑋) → ((𝑎𝐷𝑏) = 0 ↔ 𝑎 = 𝑏))
35343expb 1101 . . . 4 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑎𝑋𝑏𝑋)) → ((𝑎𝐷𝑏) = 0 ↔ 𝑎 = 𝑏))
361, 35sylan 572 . . 3 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → ((𝑎𝐷𝑏) = 0 ↔ 𝑎 = 𝑏))
3725, 33, 363bitrd 297 . 2 ((𝜑 ∧ (𝑎𝑋𝑏𝑋)) → ((𝑎(𝐹𝐷)𝑏) = 0 ↔ 𝑎 = 𝑏))
383adantr 473 . . . . 5 ((𝜑 ∧ (𝑎𝑋𝑏𝑋𝑐𝑋)) → 𝐹:(0[,]+∞)⟶ℝ*)
39123adantr3 1152 . . . . 5 ((𝜑 ∧ (𝑎𝑋𝑏𝑋𝑐𝑋)) → (𝑎𝐷𝑏) ∈ (0[,]+∞))
4038, 39ffvelrnd 6676 . . . 4 ((𝜑 ∧ (𝑎𝑋𝑏𝑋𝑐𝑋)) → (𝐹‘(𝑎𝐷𝑏)) ∈ ℝ*)
4115adantr 473 . . . . . . 7 ((𝜑 ∧ (𝑎𝑋𝑏𝑋𝑐𝑋)) → 𝐷:(𝑋 × 𝑋)⟶(0[,]+∞))
42 simpr3 1177 . . . . . . 7 ((𝜑 ∧ (𝑎𝑋𝑏𝑋𝑐𝑋)) → 𝑐𝑋)
43 simpr1 1175 . . . . . . 7 ((𝜑 ∧ (𝑎𝑋𝑏𝑋𝑐𝑋)) → 𝑎𝑋)
4441, 42, 43fovrnd 7135 . . . . . 6 ((𝜑 ∧ (𝑎𝑋𝑏𝑋𝑐𝑋)) → (𝑐𝐷𝑎) ∈ (0[,]+∞))
45 simpr2 1176 . . . . . . 7 ((𝜑 ∧ (𝑎𝑋𝑏𝑋𝑐𝑋)) → 𝑏𝑋)
4641, 42, 45fovrnd 7135 . . . . . 6 ((𝜑 ∧ (𝑎𝑋𝑏𝑋𝑐𝑋)) → (𝑐𝐷𝑏) ∈ (0[,]+∞))
47 ge0xaddcl 12665 . . . . . 6 (((𝑐𝐷𝑎) ∈ (0[,]+∞) ∧ (𝑐𝐷𝑏) ∈ (0[,]+∞)) → ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) ∈ (0[,]+∞))
4844, 46, 47syl2anc 576 . . . . 5 ((𝜑 ∧ (𝑎𝑋𝑏𝑋𝑐𝑋)) → ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) ∈ (0[,]+∞))
4938, 48ffvelrnd 6676 . . . 4 ((𝜑 ∧ (𝑎𝑋𝑏𝑋𝑐𝑋)) → (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))) ∈ ℝ*)
5038, 44ffvelrnd 6676 . . . . 5 ((𝜑 ∧ (𝑎𝑋𝑏𝑋𝑐𝑋)) → (𝐹‘(𝑐𝐷𝑎)) ∈ ℝ*)
5138, 46ffvelrnd 6676 . . . . 5 ((𝜑 ∧ (𝑎𝑋𝑏𝑋𝑐𝑋)) → (𝐹‘(𝑐𝐷𝑏)) ∈ ℝ*)
5250, 51xaddcld 12509 . . . 4 ((𝜑 ∧ (𝑎𝑋𝑏𝑋𝑐𝑋)) → ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏))) ∈ ℝ*)
53 3anrot 1082 . . . . . . 7 ((𝑐𝑋𝑎𝑋𝑏𝑋) ↔ (𝑎𝑋𝑏𝑋𝑐𝑋))
54 xmettri2 22669 . . . . . . 7 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑐𝑋𝑎𝑋𝑏𝑋)) → (𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))
5553, 54sylan2br 586 . . . . . 6 ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑎𝑋𝑏𝑋𝑐𝑋)) → (𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))
561, 55sylan 572 . . . . 5 ((𝜑 ∧ (𝑎𝑋𝑏𝑋𝑐𝑋)) → (𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))
57 comet.4 . . . . . . . 8 ((𝜑 ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞))) → (𝑥𝑦 → (𝐹𝑥) ≤ (𝐹𝑦)))
5857ralrimivva 3136 . . . . . . 7 (𝜑 → ∀𝑥 ∈ (0[,]+∞)∀𝑦 ∈ (0[,]+∞)(𝑥𝑦 → (𝐹𝑥) ≤ (𝐹𝑦)))
5958adantr 473 . . . . . 6 ((𝜑 ∧ (𝑎𝑋𝑏𝑋𝑐𝑋)) → ∀𝑥 ∈ (0[,]+∞)∀𝑦 ∈ (0[,]+∞)(𝑥𝑦 → (𝐹𝑥) ≤ (𝐹𝑦)))
60 breq1 4929 . . . . . . . 8 (𝑥 = (𝑎𝐷𝑏) → (𝑥𝑦 ↔ (𝑎𝐷𝑏) ≤ 𝑦))
6126breq1d 4936 . . . . . . . 8 (𝑥 = (𝑎𝐷𝑏) → ((𝐹𝑥) ≤ (𝐹𝑦) ↔ (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹𝑦)))
6260, 61imbi12d 337 . . . . . . 7 (𝑥 = (𝑎𝐷𝑏) → ((𝑥𝑦 → (𝐹𝑥) ≤ (𝐹𝑦)) ↔ ((𝑎𝐷𝑏) ≤ 𝑦 → (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹𝑦))))
63 breq2 4930 . . . . . . . 8 (𝑦 = ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → ((𝑎𝐷𝑏) ≤ 𝑦 ↔ (𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))))
64 fveq2 6497 . . . . . . . . 9 (𝑦 = ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → (𝐹𝑦) = (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))))
6564breq2d 4938 . . . . . . . 8 (𝑦 = ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → ((𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹𝑦) ↔ (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))))
6663, 65imbi12d 337 . . . . . . 7 (𝑦 = ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → (((𝑎𝐷𝑏) ≤ 𝑦 → (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹𝑦)) ↔ ((𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))))))
6762, 66rspc2va 3544 . . . . . 6 ((((𝑎𝐷𝑏) ∈ (0[,]+∞) ∧ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) ∈ (0[,]+∞)) ∧ ∀𝑥 ∈ (0[,]+∞)∀𝑦 ∈ (0[,]+∞)(𝑥𝑦 → (𝐹𝑥) ≤ (𝐹𝑦))) → ((𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))))
6839, 48, 59, 67syl21anc 826 . . . . 5 ((𝜑 ∧ (𝑎𝑋𝑏𝑋𝑐𝑋)) → ((𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))))
6956, 68mpd 15 . . . 4 ((𝜑 ∧ (𝑎𝑋𝑏𝑋𝑐𝑋)) → (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))))
70 comet.5 . . . . . . 7 ((𝜑 ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞))) → (𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹𝑥) +𝑒 (𝐹𝑦)))
7170ralrimivva 3136 . . . . . 6 (𝜑 → ∀𝑥 ∈ (0[,]+∞)∀𝑦 ∈ (0[,]+∞)(𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹𝑥) +𝑒 (𝐹𝑦)))
7271adantr 473 . . . . 5 ((𝜑 ∧ (𝑎𝑋𝑏𝑋𝑐𝑋)) → ∀𝑥 ∈ (0[,]+∞)∀𝑦 ∈ (0[,]+∞)(𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹𝑥) +𝑒 (𝐹𝑦)))
73 fvoveq1 6998 . . . . . . 7 (𝑥 = (𝑐𝐷𝑎) → (𝐹‘(𝑥 +𝑒 𝑦)) = (𝐹‘((𝑐𝐷𝑎) +𝑒 𝑦)))
74 fveq2 6497 . . . . . . . 8 (𝑥 = (𝑐𝐷𝑎) → (𝐹𝑥) = (𝐹‘(𝑐𝐷𝑎)))
7574oveq1d 6990 . . . . . . 7 (𝑥 = (𝑐𝐷𝑎) → ((𝐹𝑥) +𝑒 (𝐹𝑦)) = ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹𝑦)))
7673, 75breq12d 4939 . . . . . 6 (𝑥 = (𝑐𝐷𝑎) → ((𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹𝑥) +𝑒 (𝐹𝑦)) ↔ (𝐹‘((𝑐𝐷𝑎) +𝑒 𝑦)) ≤ ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹𝑦))))
77 oveq2 6983 . . . . . . . 8 (𝑦 = (𝑐𝐷𝑏) → ((𝑐𝐷𝑎) +𝑒 𝑦) = ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))
7877fveq2d 6501 . . . . . . 7 (𝑦 = (𝑐𝐷𝑏) → (𝐹‘((𝑐𝐷𝑎) +𝑒 𝑦)) = (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))))
79 fveq2 6497 . . . . . . . 8 (𝑦 = (𝑐𝐷𝑏) → (𝐹𝑦) = (𝐹‘(𝑐𝐷𝑏)))
8079oveq2d 6991 . . . . . . 7 (𝑦 = (𝑐𝐷𝑏) → ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹𝑦)) = ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏))))
8178, 80breq12d 4939 . . . . . 6 (𝑦 = (𝑐𝐷𝑏) → ((𝐹‘((𝑐𝐷𝑎) +𝑒 𝑦)) ≤ ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹𝑦)) ↔ (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))) ≤ ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏)))))
8276, 81rspc2va 3544 . . . . 5 ((((𝑐𝐷𝑎) ∈ (0[,]+∞) ∧ (𝑐𝐷𝑏) ∈ (0[,]+∞)) ∧ ∀𝑥 ∈ (0[,]+∞)∀𝑦 ∈ (0[,]+∞)(𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹𝑥) +𝑒 (𝐹𝑦))) → (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))) ≤ ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏))))
8344, 46, 72, 82syl21anc 826 . . . 4 ((𝜑 ∧ (𝑎𝑋𝑏𝑋𝑐𝑋)) → (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))) ≤ ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏))))
8440, 49, 52, 69, 83xrletrd 12371 . . 3 ((𝜑 ∧ (𝑎𝑋𝑏𝑋𝑐𝑋)) → (𝐹‘(𝑎𝐷𝑏)) ≤ ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏))))
85243adantr3 1152 . . 3 ((𝜑 ∧ (𝑎𝑋𝑏𝑋𝑐𝑋)) → (𝑎(𝐹𝐷)𝑏) = (𝐹‘(𝑎𝐷𝑏)))
865adantr 473 . . . . . 6 ((𝜑 ∧ (𝑎𝑋𝑏𝑋𝑐𝑋)) → 𝐷:(𝑋 × 𝑋)⟶ℝ*)
8742, 43opelxpd 5442 . . . . . 6 ((𝜑 ∧ (𝑎𝑋𝑏𝑋𝑐𝑋)) → ⟨𝑐, 𝑎⟩ ∈ (𝑋 × 𝑋))
88 fvco3 6587 . . . . . 6 ((𝐷:(𝑋 × 𝑋)⟶ℝ* ∧ ⟨𝑐, 𝑎⟩ ∈ (𝑋 × 𝑋)) → ((𝐹𝐷)‘⟨𝑐, 𝑎⟩) = (𝐹‘(𝐷‘⟨𝑐, 𝑎⟩)))
8986, 87, 88syl2anc 576 . . . . 5 ((𝜑 ∧ (𝑎𝑋𝑏𝑋𝑐𝑋)) → ((𝐹𝐷)‘⟨𝑐, 𝑎⟩) = (𝐹‘(𝐷‘⟨𝑐, 𝑎⟩)))
90 df-ov 6978 . . . . 5 (𝑐(𝐹𝐷)𝑎) = ((𝐹𝐷)‘⟨𝑐, 𝑎⟩)
91 df-ov 6978 . . . . . 6 (𝑐𝐷𝑎) = (𝐷‘⟨𝑐, 𝑎⟩)
9291fveq2i 6500 . . . . 5 (𝐹‘(𝑐𝐷𝑎)) = (𝐹‘(𝐷‘⟨𝑐, 𝑎⟩))
9389, 90, 923eqtr4g 2834 . . . 4 ((𝜑 ∧ (𝑎𝑋𝑏𝑋𝑐𝑋)) → (𝑐(𝐹𝐷)𝑎) = (𝐹‘(𝑐𝐷𝑎)))
9442, 45opelxpd 5442 . . . . . 6 ((𝜑 ∧ (𝑎𝑋𝑏𝑋𝑐𝑋)) → ⟨𝑐, 𝑏⟩ ∈ (𝑋 × 𝑋))
95 fvco3 6587 . . . . . 6 ((𝐷:(𝑋 × 𝑋)⟶ℝ* ∧ ⟨𝑐, 𝑏⟩ ∈ (𝑋 × 𝑋)) → ((𝐹𝐷)‘⟨𝑐, 𝑏⟩) = (𝐹‘(𝐷‘⟨𝑐, 𝑏⟩)))
9686, 94, 95syl2anc 576 . . . . 5 ((𝜑 ∧ (𝑎𝑋𝑏𝑋𝑐𝑋)) → ((𝐹𝐷)‘⟨𝑐, 𝑏⟩) = (𝐹‘(𝐷‘⟨𝑐, 𝑏⟩)))
97 df-ov 6978 . . . . 5 (𝑐(𝐹𝐷)𝑏) = ((𝐹𝐷)‘⟨𝑐, 𝑏⟩)
98 df-ov 6978 . . . . . 6 (𝑐𝐷𝑏) = (𝐷‘⟨𝑐, 𝑏⟩)
9998fveq2i 6500 . . . . 5 (𝐹‘(𝑐𝐷𝑏)) = (𝐹‘(𝐷‘⟨𝑐, 𝑏⟩))
10096, 97, 993eqtr4g 2834 . . . 4 ((𝜑 ∧ (𝑎𝑋𝑏𝑋𝑐𝑋)) → (𝑐(𝐹𝐷)𝑏) = (𝐹‘(𝑐𝐷𝑏)))
10193, 100oveq12d 6993 . . 3 ((𝜑 ∧ (𝑎𝑋𝑏𝑋𝑐𝑋)) → ((𝑐(𝐹𝐷)𝑎) +𝑒 (𝑐(𝐹𝐷)𝑏)) = ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏))))
10284, 85, 1013brtr4d 4958 . 2 ((𝜑 ∧ (𝑎𝑋𝑏𝑋𝑐𝑋)) → (𝑎(𝐹𝐷)𝑏) ≤ ((𝑐(𝐹𝐷)𝑎) +𝑒 (𝑐(𝐹𝐷)𝑏)))
1032, 17, 37, 102isxmetd 22655 1 (𝜑 → (𝐹𝐷) ∈ (∞Met‘𝑋))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 198   ∧ wa 387   ∧ w3a 1069   = wceq 1508   ∈ wcel 2051  ∀wral 3083  ⟨cop 4442   class class class wbr 4926   × cxp 5402   ∘ ccom 5408   Fn wfn 6181  ⟶wf 6182  ‘cfv 6186  (class class class)co 6975  0cc0 10334  +∞cpnf 10470  ℝ*cxr 10472   ≤ cle 10474   +𝑒 cxad 12321  [,]cicc 12556  ∞Metcxmet 20248 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1759  ax-4 1773  ax-5 1870  ax-6 1929  ax-7 1966  ax-8 2053  ax-9 2060  ax-10 2080  ax-11 2094  ax-12 2107  ax-13 2302  ax-ext 2745  ax-sep 5057  ax-nul 5064  ax-pow 5116  ax-pr 5183  ax-un 7278  ax-cnex 10390  ax-resscn 10391  ax-1cn 10392  ax-icn 10393  ax-addcl 10394  ax-addrcl 10395  ax-mulcl 10396  ax-mulrcl 10397  ax-mulcom 10398  ax-addass 10399  ax-mulass 10400  ax-distr 10401  ax-i2m1 10402  ax-1ne0 10403  ax-1rid 10404  ax-rnegex 10405  ax-rrecex 10406  ax-cnre 10407  ax-pre-lttri 10408  ax-pre-lttrn 10409  ax-pre-ltadd 10410  ax-pre-mulgt0 10411 This theorem depends on definitions:  df-bi 199  df-an 388  df-or 835  df-3or 1070  df-3an 1071  df-tru 1511  df-ex 1744  df-nf 1748  df-sb 2017  df-mo 2548  df-eu 2585  df-clab 2754  df-cleq 2766  df-clel 2841  df-nfc 2913  df-ne 2963  df-nel 3069  df-ral 3088  df-rex 3089  df-reu 3090  df-rmo 3091  df-rab 3092  df-v 3412  df-sbc 3677  df-csb 3782  df-dif 3827  df-un 3829  df-in 3831  df-ss 3838  df-nul 4174  df-if 4346  df-pw 4419  df-sn 4437  df-pr 4439  df-op 4443  df-uni 4710  df-iun 4791  df-br 4927  df-opab 4989  df-mpt 5006  df-id 5309  df-po 5323  df-so 5324  df-xp 5410  df-rel 5411  df-cnv 5412  df-co 5413  df-dm 5414  df-rn 5415  df-res 5416  df-ima 5417  df-iota 6150  df-fun 6188  df-fn 6189  df-f 6190  df-f1 6191  df-fo 6192  df-f1o 6193  df-fv 6194  df-riota 6936  df-ov 6978  df-oprab 6979  df-mpo 6980  df-1st 7500  df-2nd 7501  df-er 8088  df-map 8207  df-en 8306  df-dom 8307  df-sdom 8308  df-pnf 10475  df-mnf 10476  df-xr 10477  df-ltxr 10478  df-le 10479  df-sub 10671  df-neg 10672  df-div 11098  df-2 11502  df-rp 12204  df-xneg 12323  df-xadd 12324  df-xmul 12325  df-icc 12560  df-xmet 20256 This theorem is referenced by:  stdbdxmet  22844
 Copyright terms: Public domain W3C validator