Step | Hyp | Ref
| Expression |
1 | | xmetrel 13137 |
. . . 4
⊢ Rel
∞Met |
2 | | comet.1 |
. . . 4
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) |
3 | | relelfvdm 5528 |
. . . 4
⊢ ((Rel
∞Met ∧ 𝐷 ∈
(∞Met‘𝑋))
→ 𝑋 ∈ dom
∞Met) |
4 | 1, 2, 3 | sylancr 412 |
. . 3
⊢ (𝜑 → 𝑋 ∈ dom ∞Met) |
5 | 4 | elexd 2743 |
. 2
⊢ (𝜑 → 𝑋 ∈ V) |
6 | | comet.2 |
. . 3
⊢ (𝜑 → 𝐹:(0[,]+∞)⟶ℝ*) |
7 | | xmetf 13144 |
. . . . . 6
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*) |
8 | 2, 7 | syl 14 |
. . . . 5
⊢ (𝜑 → 𝐷:(𝑋 × 𝑋)⟶ℝ*) |
9 | 8 | ffnd 5348 |
. . . 4
⊢ (𝜑 → 𝐷 Fn (𝑋 × 𝑋)) |
10 | | xmetcl 13146 |
. . . . . . . 8
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (𝑎𝐷𝑏) ∈
ℝ*) |
11 | | xmetge0 13159 |
. . . . . . . 8
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → 0 ≤ (𝑎𝐷𝑏)) |
12 | | elxrge0 9935 |
. . . . . . . 8
⊢ ((𝑎𝐷𝑏) ∈ (0[,]+∞) ↔ ((𝑎𝐷𝑏) ∈ ℝ* ∧ 0 ≤
(𝑎𝐷𝑏))) |
13 | 10, 11, 12 | sylanbrc 415 |
. . . . . . 7
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (𝑎𝐷𝑏) ∈ (0[,]+∞)) |
14 | 13 | 3expb 1199 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑎𝐷𝑏) ∈ (0[,]+∞)) |
15 | 2, 14 | sylan 281 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑎𝐷𝑏) ∈ (0[,]+∞)) |
16 | 15 | ralrimivva 2552 |
. . . 4
⊢ (𝜑 → ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎𝐷𝑏) ∈ (0[,]+∞)) |
17 | | ffnov 5957 |
. . . 4
⊢ (𝐷:(𝑋 × 𝑋)⟶(0[,]+∞) ↔ (𝐷 Fn (𝑋 × 𝑋) ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎𝐷𝑏) ∈ (0[,]+∞))) |
18 | 9, 16, 17 | sylanbrc 415 |
. . 3
⊢ (𝜑 → 𝐷:(𝑋 × 𝑋)⟶(0[,]+∞)) |
19 | | fco 5363 |
. . 3
⊢ ((𝐹:(0[,]+∞)⟶ℝ*
∧ 𝐷:(𝑋 × 𝑋)⟶(0[,]+∞)) → (𝐹 ∘ 𝐷):(𝑋 × 𝑋)⟶ℝ*) |
20 | 6, 18, 19 | syl2anc 409 |
. 2
⊢ (𝜑 → (𝐹 ∘ 𝐷):(𝑋 × 𝑋)⟶ℝ*) |
21 | | opelxpi 4643 |
. . . . . 6
⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → 〈𝑎, 𝑏〉 ∈ (𝑋 × 𝑋)) |
22 | | fvco3 5567 |
. . . . . 6
⊢ ((𝐷:(𝑋 × 𝑋)⟶ℝ* ∧
〈𝑎, 𝑏〉 ∈ (𝑋 × 𝑋)) → ((𝐹 ∘ 𝐷)‘〈𝑎, 𝑏〉) = (𝐹‘(𝐷‘〈𝑎, 𝑏〉))) |
23 | 8, 21, 22 | syl2an 287 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝐹 ∘ 𝐷)‘〈𝑎, 𝑏〉) = (𝐹‘(𝐷‘〈𝑎, 𝑏〉))) |
24 | | df-ov 5856 |
. . . . 5
⊢ (𝑎(𝐹 ∘ 𝐷)𝑏) = ((𝐹 ∘ 𝐷)‘〈𝑎, 𝑏〉) |
25 | | df-ov 5856 |
. . . . . 6
⊢ (𝑎𝐷𝑏) = (𝐷‘〈𝑎, 𝑏〉) |
26 | 25 | fveq2i 5499 |
. . . . 5
⊢ (𝐹‘(𝑎𝐷𝑏)) = (𝐹‘(𝐷‘〈𝑎, 𝑏〉)) |
27 | 23, 24, 26 | 3eqtr4g 2228 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑎(𝐹 ∘ 𝐷)𝑏) = (𝐹‘(𝑎𝐷𝑏))) |
28 | 27 | eqeq1d 2179 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑎(𝐹 ∘ 𝐷)𝑏) = 0 ↔ (𝐹‘(𝑎𝐷𝑏)) = 0)) |
29 | | fveq2 5496 |
. . . . . 6
⊢ (𝑥 = (𝑎𝐷𝑏) → (𝐹‘𝑥) = (𝐹‘(𝑎𝐷𝑏))) |
30 | 29 | eqeq1d 2179 |
. . . . 5
⊢ (𝑥 = (𝑎𝐷𝑏) → ((𝐹‘𝑥) = 0 ↔ (𝐹‘(𝑎𝐷𝑏)) = 0)) |
31 | | eqeq1 2177 |
. . . . 5
⊢ (𝑥 = (𝑎𝐷𝑏) → (𝑥 = 0 ↔ (𝑎𝐷𝑏) = 0)) |
32 | 30, 31 | bibi12d 234 |
. . . 4
⊢ (𝑥 = (𝑎𝐷𝑏) → (((𝐹‘𝑥) = 0 ↔ 𝑥 = 0) ↔ ((𝐹‘(𝑎𝐷𝑏)) = 0 ↔ (𝑎𝐷𝑏) = 0))) |
33 | | comet.3 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞)) → ((𝐹‘𝑥) = 0 ↔ 𝑥 = 0)) |
34 | 33 | ralrimiva 2543 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ (0[,]+∞)((𝐹‘𝑥) = 0 ↔ 𝑥 = 0)) |
35 | 34 | adantr 274 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ∀𝑥 ∈ (0[,]+∞)((𝐹‘𝑥) = 0 ↔ 𝑥 = 0)) |
36 | 32, 35, 15 | rspcdva 2839 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝐹‘(𝑎𝐷𝑏)) = 0 ↔ (𝑎𝐷𝑏) = 0)) |
37 | | xmeteq0 13153 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → ((𝑎𝐷𝑏) = 0 ↔ 𝑎 = 𝑏)) |
38 | 37 | 3expb 1199 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑎𝐷𝑏) = 0 ↔ 𝑎 = 𝑏)) |
39 | 2, 38 | sylan 281 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑎𝐷𝑏) = 0 ↔ 𝑎 = 𝑏)) |
40 | 28, 36, 39 | 3bitrd 213 |
. 2
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑎(𝐹 ∘ 𝐷)𝑏) = 0 ↔ 𝑎 = 𝑏)) |
41 | 6 | adantr 274 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝐹:(0[,]+∞)⟶ℝ*) |
42 | 15 | 3adantr3 1153 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑎𝐷𝑏) ∈ (0[,]+∞)) |
43 | 41, 42 | ffvelrnd 5632 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑎𝐷𝑏)) ∈
ℝ*) |
44 | 18 | adantr 274 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝐷:(𝑋 × 𝑋)⟶(0[,]+∞)) |
45 | | simpr3 1000 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝑐 ∈ 𝑋) |
46 | | simpr1 998 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝑎 ∈ 𝑋) |
47 | 44, 45, 46 | fovrnd 5997 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑐𝐷𝑎) ∈ (0[,]+∞)) |
48 | | simpr2 999 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝑏 ∈ 𝑋) |
49 | 44, 45, 48 | fovrnd 5997 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑐𝐷𝑏) ∈ (0[,]+∞)) |
50 | | ge0xaddcl 9940 |
. . . . . 6
⊢ (((𝑐𝐷𝑎) ∈ (0[,]+∞) ∧ (𝑐𝐷𝑏) ∈ (0[,]+∞)) → ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) ∈ (0[,]+∞)) |
51 | 47, 49, 50 | syl2anc 409 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) ∈ (0[,]+∞)) |
52 | 41, 51 | ffvelrnd 5632 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))) ∈
ℝ*) |
53 | 41, 47 | ffvelrnd 5632 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑐𝐷𝑎)) ∈
ℝ*) |
54 | 41, 49 | ffvelrnd 5632 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑐𝐷𝑏)) ∈
ℝ*) |
55 | 53, 54 | xaddcld 9841 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏))) ∈
ℝ*) |
56 | | 3anrot 978 |
. . . . . . 7
⊢ ((𝑐 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ↔ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) |
57 | | xmettri2 13155 |
. . . . . . 7
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑐 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))) |
58 | 56, 57 | sylan2br 286 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))) |
59 | 2, 58 | sylan 281 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))) |
60 | | comet.4 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞))) →
(𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦))) |
61 | 60 | ralrimivva 2552 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ (0[,]+∞)∀𝑦 ∈ (0[,]+∞)(𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦))) |
62 | 61 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ∀𝑥 ∈ (0[,]+∞)∀𝑦 ∈ (0[,]+∞)(𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦))) |
63 | | breq1 3992 |
. . . . . . . 8
⊢ (𝑥 = (𝑎𝐷𝑏) → (𝑥 ≤ 𝑦 ↔ (𝑎𝐷𝑏) ≤ 𝑦)) |
64 | 29 | breq1d 3999 |
. . . . . . . 8
⊢ (𝑥 = (𝑎𝐷𝑏) → ((𝐹‘𝑥) ≤ (𝐹‘𝑦) ↔ (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘𝑦))) |
65 | 63, 64 | imbi12d 233 |
. . . . . . 7
⊢ (𝑥 = (𝑎𝐷𝑏) → ((𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦)) ↔ ((𝑎𝐷𝑏) ≤ 𝑦 → (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘𝑦)))) |
66 | | breq2 3993 |
. . . . . . . 8
⊢ (𝑦 = ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → ((𝑎𝐷𝑏) ≤ 𝑦 ↔ (𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))) |
67 | | fveq2 5496 |
. . . . . . . . 9
⊢ (𝑦 = ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → (𝐹‘𝑦) = (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))) |
68 | 67 | breq2d 4001 |
. . . . . . . 8
⊢ (𝑦 = ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → ((𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘𝑦) ↔ (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))))) |
69 | 66, 68 | imbi12d 233 |
. . . . . . 7
⊢ (𝑦 = ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → (((𝑎𝐷𝑏) ≤ 𝑦 → (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘𝑦)) ↔ ((𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))))) |
70 | 65, 69 | rspc2va 2848 |
. . . . . 6
⊢ ((((𝑎𝐷𝑏) ∈ (0[,]+∞) ∧ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) ∈ (0[,]+∞)) ∧ ∀𝑥 ∈
(0[,]+∞)∀𝑦
∈ (0[,]+∞)(𝑥
≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦))) → ((𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))))) |
71 | 42, 51, 62, 70 | syl21anc 1232 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))))) |
72 | 59, 71 | mpd 13 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))) |
73 | | comet.5 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞))) →
(𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹‘𝑥) +𝑒 (𝐹‘𝑦))) |
74 | 73 | ralrimivva 2552 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ (0[,]+∞)∀𝑦 ∈ (0[,]+∞)(𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹‘𝑥) +𝑒 (𝐹‘𝑦))) |
75 | 74 | adantr 274 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ∀𝑥 ∈ (0[,]+∞)∀𝑦 ∈ (0[,]+∞)(𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹‘𝑥) +𝑒 (𝐹‘𝑦))) |
76 | | fvoveq1 5876 |
. . . . . . 7
⊢ (𝑥 = (𝑐𝐷𝑎) → (𝐹‘(𝑥 +𝑒 𝑦)) = (𝐹‘((𝑐𝐷𝑎) +𝑒 𝑦))) |
77 | | fveq2 5496 |
. . . . . . . 8
⊢ (𝑥 = (𝑐𝐷𝑎) → (𝐹‘𝑥) = (𝐹‘(𝑐𝐷𝑎))) |
78 | 77 | oveq1d 5868 |
. . . . . . 7
⊢ (𝑥 = (𝑐𝐷𝑎) → ((𝐹‘𝑥) +𝑒 (𝐹‘𝑦)) = ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘𝑦))) |
79 | 76, 78 | breq12d 4002 |
. . . . . 6
⊢ (𝑥 = (𝑐𝐷𝑎) → ((𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹‘𝑥) +𝑒 (𝐹‘𝑦)) ↔ (𝐹‘((𝑐𝐷𝑎) +𝑒 𝑦)) ≤ ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘𝑦)))) |
80 | | oveq2 5861 |
. . . . . . . 8
⊢ (𝑦 = (𝑐𝐷𝑏) → ((𝑐𝐷𝑎) +𝑒 𝑦) = ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))) |
81 | 80 | fveq2d 5500 |
. . . . . . 7
⊢ (𝑦 = (𝑐𝐷𝑏) → (𝐹‘((𝑐𝐷𝑎) +𝑒 𝑦)) = (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))) |
82 | | fveq2 5496 |
. . . . . . . 8
⊢ (𝑦 = (𝑐𝐷𝑏) → (𝐹‘𝑦) = (𝐹‘(𝑐𝐷𝑏))) |
83 | 82 | oveq2d 5869 |
. . . . . . 7
⊢ (𝑦 = (𝑐𝐷𝑏) → ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘𝑦)) = ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏)))) |
84 | 81, 83 | breq12d 4002 |
. . . . . 6
⊢ (𝑦 = (𝑐𝐷𝑏) → ((𝐹‘((𝑐𝐷𝑎) +𝑒 𝑦)) ≤ ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘𝑦)) ↔ (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))) ≤ ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏))))) |
85 | 79, 84 | rspc2va 2848 |
. . . . 5
⊢ ((((𝑐𝐷𝑎) ∈ (0[,]+∞) ∧ (𝑐𝐷𝑏) ∈ (0[,]+∞)) ∧ ∀𝑥 ∈
(0[,]+∞)∀𝑦
∈ (0[,]+∞)(𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹‘𝑥) +𝑒 (𝐹‘𝑦))) → (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))) ≤ ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏)))) |
86 | 47, 49, 75, 85 | syl21anc 1232 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))) ≤ ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏)))) |
87 | 43, 52, 55, 72, 86 | xrletrd 9769 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑎𝐷𝑏)) ≤ ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏)))) |
88 | 27 | 3adantr3 1153 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑎(𝐹 ∘ 𝐷)𝑏) = (𝐹‘(𝑎𝐷𝑏))) |
89 | 8 | adantr 274 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝐷:(𝑋 × 𝑋)⟶ℝ*) |
90 | 45, 46 | opelxpd 4644 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 〈𝑐, 𝑎〉 ∈ (𝑋 × 𝑋)) |
91 | | fvco3 5567 |
. . . . . 6
⊢ ((𝐷:(𝑋 × 𝑋)⟶ℝ* ∧
〈𝑐, 𝑎〉 ∈ (𝑋 × 𝑋)) → ((𝐹 ∘ 𝐷)‘〈𝑐, 𝑎〉) = (𝐹‘(𝐷‘〈𝑐, 𝑎〉))) |
92 | 89, 90, 91 | syl2anc 409 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝐹 ∘ 𝐷)‘〈𝑐, 𝑎〉) = (𝐹‘(𝐷‘〈𝑐, 𝑎〉))) |
93 | | df-ov 5856 |
. . . . 5
⊢ (𝑐(𝐹 ∘ 𝐷)𝑎) = ((𝐹 ∘ 𝐷)‘〈𝑐, 𝑎〉) |
94 | | df-ov 5856 |
. . . . . 6
⊢ (𝑐𝐷𝑎) = (𝐷‘〈𝑐, 𝑎〉) |
95 | 94 | fveq2i 5499 |
. . . . 5
⊢ (𝐹‘(𝑐𝐷𝑎)) = (𝐹‘(𝐷‘〈𝑐, 𝑎〉)) |
96 | 92, 93, 95 | 3eqtr4g 2228 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑐(𝐹 ∘ 𝐷)𝑎) = (𝐹‘(𝑐𝐷𝑎))) |
97 | 45, 48 | opelxpd 4644 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 〈𝑐, 𝑏〉 ∈ (𝑋 × 𝑋)) |
98 | | fvco3 5567 |
. . . . . 6
⊢ ((𝐷:(𝑋 × 𝑋)⟶ℝ* ∧
〈𝑐, 𝑏〉 ∈ (𝑋 × 𝑋)) → ((𝐹 ∘ 𝐷)‘〈𝑐, 𝑏〉) = (𝐹‘(𝐷‘〈𝑐, 𝑏〉))) |
99 | 89, 97, 98 | syl2anc 409 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝐹 ∘ 𝐷)‘〈𝑐, 𝑏〉) = (𝐹‘(𝐷‘〈𝑐, 𝑏〉))) |
100 | | df-ov 5856 |
. . . . 5
⊢ (𝑐(𝐹 ∘ 𝐷)𝑏) = ((𝐹 ∘ 𝐷)‘〈𝑐, 𝑏〉) |
101 | | df-ov 5856 |
. . . . . 6
⊢ (𝑐𝐷𝑏) = (𝐷‘〈𝑐, 𝑏〉) |
102 | 101 | fveq2i 5499 |
. . . . 5
⊢ (𝐹‘(𝑐𝐷𝑏)) = (𝐹‘(𝐷‘〈𝑐, 𝑏〉)) |
103 | 99, 100, 102 | 3eqtr4g 2228 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑐(𝐹 ∘ 𝐷)𝑏) = (𝐹‘(𝑐𝐷𝑏))) |
104 | 96, 103 | oveq12d 5871 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝑐(𝐹 ∘ 𝐷)𝑎) +𝑒 (𝑐(𝐹 ∘ 𝐷)𝑏)) = ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏)))) |
105 | 87, 88, 104 | 3brtr4d 4021 |
. 2
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑎(𝐹 ∘ 𝐷)𝑏) ≤ ((𝑐(𝐹 ∘ 𝐷)𝑎) +𝑒 (𝑐(𝐹 ∘ 𝐷)𝑏))) |
106 | 5, 20, 40, 105 | isxmetd 13141 |
1
⊢ (𝜑 → (𝐹 ∘ 𝐷) ∈ (∞Met‘𝑋)) |