Step | Hyp | Ref
| Expression |
1 | | comet.1 |
. . 3
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) |
2 | 1 | elfvexd 6222 |
. 2
⊢ (𝜑 → 𝑋 ∈ V) |
3 | | comet.2 |
. . 3
⊢ (𝜑 → 𝐹:(0[,]+∞)⟶ℝ*) |
4 | | xmetf 22134 |
. . . . . 6
⊢ (𝐷 ∈ (∞Met‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*) |
5 | 1, 4 | syl 17 |
. . . . 5
⊢ (𝜑 → 𝐷:(𝑋 × 𝑋)⟶ℝ*) |
6 | | ffn 6045 |
. . . . 5
⊢ (𝐷:(𝑋 × 𝑋)⟶ℝ* → 𝐷 Fn (𝑋 × 𝑋)) |
7 | 5, 6 | syl 17 |
. . . 4
⊢ (𝜑 → 𝐷 Fn (𝑋 × 𝑋)) |
8 | | xmetcl 22136 |
. . . . . . . 8
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (𝑎𝐷𝑏) ∈
ℝ*) |
9 | | xmetge0 22149 |
. . . . . . . 8
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → 0 ≤ (𝑎𝐷𝑏)) |
10 | | elxrge0 12281 |
. . . . . . . 8
⊢ ((𝑎𝐷𝑏) ∈ (0[,]+∞) ↔ ((𝑎𝐷𝑏) ∈ ℝ* ∧ 0 ≤
(𝑎𝐷𝑏))) |
11 | 8, 9, 10 | sylanbrc 698 |
. . . . . . 7
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → (𝑎𝐷𝑏) ∈ (0[,]+∞)) |
12 | 11 | 3expb 1266 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑎𝐷𝑏) ∈ (0[,]+∞)) |
13 | 1, 12 | sylan 488 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑎𝐷𝑏) ∈ (0[,]+∞)) |
14 | 13 | ralrimivva 2971 |
. . . 4
⊢ (𝜑 → ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎𝐷𝑏) ∈ (0[,]+∞)) |
15 | | ffnov 6764 |
. . . 4
⊢ (𝐷:(𝑋 × 𝑋)⟶(0[,]+∞) ↔ (𝐷 Fn (𝑋 × 𝑋) ∧ ∀𝑎 ∈ 𝑋 ∀𝑏 ∈ 𝑋 (𝑎𝐷𝑏) ∈ (0[,]+∞))) |
16 | 7, 14, 15 | sylanbrc 698 |
. . 3
⊢ (𝜑 → 𝐷:(𝑋 × 𝑋)⟶(0[,]+∞)) |
17 | | fco 6058 |
. . 3
⊢ ((𝐹:(0[,]+∞)⟶ℝ*
∧ 𝐷:(𝑋 × 𝑋)⟶(0[,]+∞)) → (𝐹 ∘ 𝐷):(𝑋 × 𝑋)⟶ℝ*) |
18 | 3, 16, 17 | syl2anc 693 |
. 2
⊢ (𝜑 → (𝐹 ∘ 𝐷):(𝑋 × 𝑋)⟶ℝ*) |
19 | | opelxpi 5148 |
. . . . . 6
⊢ ((𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → 〈𝑎, 𝑏〉 ∈ (𝑋 × 𝑋)) |
20 | | fvco3 6275 |
. . . . . 6
⊢ ((𝐷:(𝑋 × 𝑋)⟶ℝ* ∧
〈𝑎, 𝑏〉 ∈ (𝑋 × 𝑋)) → ((𝐹 ∘ 𝐷)‘〈𝑎, 𝑏〉) = (𝐹‘(𝐷‘〈𝑎, 𝑏〉))) |
21 | 5, 19, 20 | syl2an 494 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝐹 ∘ 𝐷)‘〈𝑎, 𝑏〉) = (𝐹‘(𝐷‘〈𝑎, 𝑏〉))) |
22 | | df-ov 6653 |
. . . . 5
⊢ (𝑎(𝐹 ∘ 𝐷)𝑏) = ((𝐹 ∘ 𝐷)‘〈𝑎, 𝑏〉) |
23 | | df-ov 6653 |
. . . . . 6
⊢ (𝑎𝐷𝑏) = (𝐷‘〈𝑎, 𝑏〉) |
24 | 23 | fveq2i 6194 |
. . . . 5
⊢ (𝐹‘(𝑎𝐷𝑏)) = (𝐹‘(𝐷‘〈𝑎, 𝑏〉)) |
25 | 21, 22, 24 | 3eqtr4g 2681 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑎(𝐹 ∘ 𝐷)𝑏) = (𝐹‘(𝑎𝐷𝑏))) |
26 | 25 | eqeq1d 2624 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑎(𝐹 ∘ 𝐷)𝑏) = 0 ↔ (𝐹‘(𝑎𝐷𝑏)) = 0)) |
27 | | comet.3 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (0[,]+∞)) → ((𝐹‘𝑥) = 0 ↔ 𝑥 = 0)) |
28 | 27 | ralrimiva 2966 |
. . . . 5
⊢ (𝜑 → ∀𝑥 ∈ (0[,]+∞)((𝐹‘𝑥) = 0 ↔ 𝑥 = 0)) |
29 | 28 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ∀𝑥 ∈ (0[,]+∞)((𝐹‘𝑥) = 0 ↔ 𝑥 = 0)) |
30 | | fveq2 6191 |
. . . . . . 7
⊢ (𝑥 = (𝑎𝐷𝑏) → (𝐹‘𝑥) = (𝐹‘(𝑎𝐷𝑏))) |
31 | 30 | eqeq1d 2624 |
. . . . . 6
⊢ (𝑥 = (𝑎𝐷𝑏) → ((𝐹‘𝑥) = 0 ↔ (𝐹‘(𝑎𝐷𝑏)) = 0)) |
32 | | eqeq1 2626 |
. . . . . 6
⊢ (𝑥 = (𝑎𝐷𝑏) → (𝑥 = 0 ↔ (𝑎𝐷𝑏) = 0)) |
33 | 31, 32 | bibi12d 335 |
. . . . 5
⊢ (𝑥 = (𝑎𝐷𝑏) → (((𝐹‘𝑥) = 0 ↔ 𝑥 = 0) ↔ ((𝐹‘(𝑎𝐷𝑏)) = 0 ↔ (𝑎𝐷𝑏) = 0))) |
34 | 33 | rspcv 3305 |
. . . 4
⊢ ((𝑎𝐷𝑏) ∈ (0[,]+∞) → (∀𝑥 ∈ (0[,]+∞)((𝐹‘𝑥) = 0 ↔ 𝑥 = 0) → ((𝐹‘(𝑎𝐷𝑏)) = 0 ↔ (𝑎𝐷𝑏) = 0))) |
35 | 13, 29, 34 | sylc 65 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝐹‘(𝑎𝐷𝑏)) = 0 ↔ (𝑎𝐷𝑏) = 0)) |
36 | | xmeteq0 22143 |
. . . . 5
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → ((𝑎𝐷𝑏) = 0 ↔ 𝑎 = 𝑏)) |
37 | 36 | 3expb 1266 |
. . . 4
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑎𝐷𝑏) = 0 ↔ 𝑎 = 𝑏)) |
38 | 1, 37 | sylan 488 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑎𝐷𝑏) = 0 ↔ 𝑎 = 𝑏)) |
39 | 26, 35, 38 | 3bitrd 294 |
. 2
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → ((𝑎(𝐹 ∘ 𝐷)𝑏) = 0 ↔ 𝑎 = 𝑏)) |
40 | 3 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝐹:(0[,]+∞)⟶ℝ*) |
41 | 13 | 3adantr3 1222 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑎𝐷𝑏) ∈ (0[,]+∞)) |
42 | 40, 41 | ffvelrnd 6360 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑎𝐷𝑏)) ∈
ℝ*) |
43 | 16 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝐷:(𝑋 × 𝑋)⟶(0[,]+∞)) |
44 | | simpr3 1069 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝑐 ∈ 𝑋) |
45 | | simpr1 1067 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝑎 ∈ 𝑋) |
46 | 43, 44, 45 | fovrnd 6806 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑐𝐷𝑎) ∈ (0[,]+∞)) |
47 | | simpr2 1068 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝑏 ∈ 𝑋) |
48 | 43, 44, 47 | fovrnd 6806 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑐𝐷𝑏) ∈ (0[,]+∞)) |
49 | | ge0xaddcl 12286 |
. . . . . 6
⊢ (((𝑐𝐷𝑎) ∈ (0[,]+∞) ∧ (𝑐𝐷𝑏) ∈ (0[,]+∞)) → ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) ∈ (0[,]+∞)) |
50 | 46, 48, 49 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) ∈ (0[,]+∞)) |
51 | 40, 50 | ffvelrnd 6360 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))) ∈
ℝ*) |
52 | 40, 46 | ffvelrnd 6360 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑐𝐷𝑎)) ∈
ℝ*) |
53 | 40, 48 | ffvelrnd 6360 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑐𝐷𝑏)) ∈
ℝ*) |
54 | 52, 53 | xaddcld 12131 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏))) ∈
ℝ*) |
55 | | 3anrot 1043 |
. . . . . . 7
⊢ ((𝑐 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) ↔ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) |
56 | | xmettri2 22145 |
. . . . . . 7
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑐 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))) |
57 | 55, 56 | sylan2br 493 |
. . . . . 6
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))) |
58 | 1, 57 | sylan 488 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))) |
59 | | comet.4 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞))) →
(𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦))) |
60 | 59 | ralrimivva 2971 |
. . . . . . 7
⊢ (𝜑 → ∀𝑥 ∈ (0[,]+∞)∀𝑦 ∈ (0[,]+∞)(𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦))) |
61 | 60 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ∀𝑥 ∈ (0[,]+∞)∀𝑦 ∈ (0[,]+∞)(𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦))) |
62 | | breq1 4656 |
. . . . . . . 8
⊢ (𝑥 = (𝑎𝐷𝑏) → (𝑥 ≤ 𝑦 ↔ (𝑎𝐷𝑏) ≤ 𝑦)) |
63 | 30 | breq1d 4663 |
. . . . . . . 8
⊢ (𝑥 = (𝑎𝐷𝑏) → ((𝐹‘𝑥) ≤ (𝐹‘𝑦) ↔ (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘𝑦))) |
64 | 62, 63 | imbi12d 334 |
. . . . . . 7
⊢ (𝑥 = (𝑎𝐷𝑏) → ((𝑥 ≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦)) ↔ ((𝑎𝐷𝑏) ≤ 𝑦 → (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘𝑦)))) |
65 | | breq2 4657 |
. . . . . . . 8
⊢ (𝑦 = ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → ((𝑎𝐷𝑏) ≤ 𝑦 ↔ (𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))) |
66 | | fveq2 6191 |
. . . . . . . . 9
⊢ (𝑦 = ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → (𝐹‘𝑦) = (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))) |
67 | 66 | breq2d 4665 |
. . . . . . . 8
⊢ (𝑦 = ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → ((𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘𝑦) ↔ (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))))) |
68 | 65, 67 | imbi12d 334 |
. . . . . . 7
⊢ (𝑦 = ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → (((𝑎𝐷𝑏) ≤ 𝑦 → (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘𝑦)) ↔ ((𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))))) |
69 | 64, 68 | rspc2va 3323 |
. . . . . 6
⊢ ((((𝑎𝐷𝑏) ∈ (0[,]+∞) ∧ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) ∈ (0[,]+∞)) ∧ ∀𝑥 ∈
(0[,]+∞)∀𝑦
∈ (0[,]+∞)(𝑥
≤ 𝑦 → (𝐹‘𝑥) ≤ (𝐹‘𝑦))) → ((𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))))) |
70 | 41, 50, 61, 69 | syl21anc 1325 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)) → (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))))) |
71 | 58, 70 | mpd 15 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑎𝐷𝑏)) ≤ (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))) |
72 | | comet.5 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (0[,]+∞) ∧ 𝑦 ∈ (0[,]+∞))) →
(𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹‘𝑥) +𝑒 (𝐹‘𝑦))) |
73 | 72 | ralrimivva 2971 |
. . . . . 6
⊢ (𝜑 → ∀𝑥 ∈ (0[,]+∞)∀𝑦 ∈ (0[,]+∞)(𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹‘𝑥) +𝑒 (𝐹‘𝑦))) |
74 | 73 | adantr 481 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ∀𝑥 ∈ (0[,]+∞)∀𝑦 ∈ (0[,]+∞)(𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹‘𝑥) +𝑒 (𝐹‘𝑦))) |
75 | | oveq1 6657 |
. . . . . . . 8
⊢ (𝑥 = (𝑐𝐷𝑎) → (𝑥 +𝑒 𝑦) = ((𝑐𝐷𝑎) +𝑒 𝑦)) |
76 | 75 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑥 = (𝑐𝐷𝑎) → (𝐹‘(𝑥 +𝑒 𝑦)) = (𝐹‘((𝑐𝐷𝑎) +𝑒 𝑦))) |
77 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑥 = (𝑐𝐷𝑎) → (𝐹‘𝑥) = (𝐹‘(𝑐𝐷𝑎))) |
78 | 77 | oveq1d 6665 |
. . . . . . 7
⊢ (𝑥 = (𝑐𝐷𝑎) → ((𝐹‘𝑥) +𝑒 (𝐹‘𝑦)) = ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘𝑦))) |
79 | 76, 78 | breq12d 4666 |
. . . . . 6
⊢ (𝑥 = (𝑐𝐷𝑎) → ((𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹‘𝑥) +𝑒 (𝐹‘𝑦)) ↔ (𝐹‘((𝑐𝐷𝑎) +𝑒 𝑦)) ≤ ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘𝑦)))) |
80 | | oveq2 6658 |
. . . . . . . 8
⊢ (𝑦 = (𝑐𝐷𝑏) → ((𝑐𝐷𝑎) +𝑒 𝑦) = ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))) |
81 | 80 | fveq2d 6195 |
. . . . . . 7
⊢ (𝑦 = (𝑐𝐷𝑏) → (𝐹‘((𝑐𝐷𝑎) +𝑒 𝑦)) = (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏)))) |
82 | | fveq2 6191 |
. . . . . . . 8
⊢ (𝑦 = (𝑐𝐷𝑏) → (𝐹‘𝑦) = (𝐹‘(𝑐𝐷𝑏))) |
83 | 82 | oveq2d 6666 |
. . . . . . 7
⊢ (𝑦 = (𝑐𝐷𝑏) → ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘𝑦)) = ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏)))) |
84 | 81, 83 | breq12d 4666 |
. . . . . 6
⊢ (𝑦 = (𝑐𝐷𝑏) → ((𝐹‘((𝑐𝐷𝑎) +𝑒 𝑦)) ≤ ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘𝑦)) ↔ (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))) ≤ ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏))))) |
85 | 79, 84 | rspc2va 3323 |
. . . . 5
⊢ ((((𝑐𝐷𝑎) ∈ (0[,]+∞) ∧ (𝑐𝐷𝑏) ∈ (0[,]+∞)) ∧ ∀𝑥 ∈
(0[,]+∞)∀𝑦
∈ (0[,]+∞)(𝐹‘(𝑥 +𝑒 𝑦)) ≤ ((𝐹‘𝑥) +𝑒 (𝐹‘𝑦))) → (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))) ≤ ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏)))) |
86 | 46, 48, 74, 85 | syl21anc 1325 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))) ≤ ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏)))) |
87 | 42, 51, 54, 71, 86 | xrletrd 11993 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝐹‘(𝑎𝐷𝑏)) ≤ ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏)))) |
88 | 25 | 3adantr3 1222 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑎(𝐹 ∘ 𝐷)𝑏) = (𝐹‘(𝑎𝐷𝑏))) |
89 | 5 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 𝐷:(𝑋 × 𝑋)⟶ℝ*) |
90 | | opelxpi 5148 |
. . . . . . 7
⊢ ((𝑐 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋) → 〈𝑐, 𝑎〉 ∈ (𝑋 × 𝑋)) |
91 | 44, 45, 90 | syl2anc 693 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 〈𝑐, 𝑎〉 ∈ (𝑋 × 𝑋)) |
92 | | fvco3 6275 |
. . . . . 6
⊢ ((𝐷:(𝑋 × 𝑋)⟶ℝ* ∧
〈𝑐, 𝑎〉 ∈ (𝑋 × 𝑋)) → ((𝐹 ∘ 𝐷)‘〈𝑐, 𝑎〉) = (𝐹‘(𝐷‘〈𝑐, 𝑎〉))) |
93 | 89, 91, 92 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝐹 ∘ 𝐷)‘〈𝑐, 𝑎〉) = (𝐹‘(𝐷‘〈𝑐, 𝑎〉))) |
94 | | df-ov 6653 |
. . . . 5
⊢ (𝑐(𝐹 ∘ 𝐷)𝑎) = ((𝐹 ∘ 𝐷)‘〈𝑐, 𝑎〉) |
95 | | df-ov 6653 |
. . . . . 6
⊢ (𝑐𝐷𝑎) = (𝐷‘〈𝑐, 𝑎〉) |
96 | 95 | fveq2i 6194 |
. . . . 5
⊢ (𝐹‘(𝑐𝐷𝑎)) = (𝐹‘(𝐷‘〈𝑐, 𝑎〉)) |
97 | 93, 94, 96 | 3eqtr4g 2681 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑐(𝐹 ∘ 𝐷)𝑎) = (𝐹‘(𝑐𝐷𝑎))) |
98 | | opelxpi 5148 |
. . . . . . 7
⊢ ((𝑐 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋) → 〈𝑐, 𝑏〉 ∈ (𝑋 × 𝑋)) |
99 | 44, 47, 98 | syl2anc 693 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → 〈𝑐, 𝑏〉 ∈ (𝑋 × 𝑋)) |
100 | | fvco3 6275 |
. . . . . 6
⊢ ((𝐷:(𝑋 × 𝑋)⟶ℝ* ∧
〈𝑐, 𝑏〉 ∈ (𝑋 × 𝑋)) → ((𝐹 ∘ 𝐷)‘〈𝑐, 𝑏〉) = (𝐹‘(𝐷‘〈𝑐, 𝑏〉))) |
101 | 89, 99, 100 | syl2anc 693 |
. . . . 5
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝐹 ∘ 𝐷)‘〈𝑐, 𝑏〉) = (𝐹‘(𝐷‘〈𝑐, 𝑏〉))) |
102 | | df-ov 6653 |
. . . . 5
⊢ (𝑐(𝐹 ∘ 𝐷)𝑏) = ((𝐹 ∘ 𝐷)‘〈𝑐, 𝑏〉) |
103 | | df-ov 6653 |
. . . . . 6
⊢ (𝑐𝐷𝑏) = (𝐷‘〈𝑐, 𝑏〉) |
104 | 103 | fveq2i 6194 |
. . . . 5
⊢ (𝐹‘(𝑐𝐷𝑏)) = (𝐹‘(𝐷‘〈𝑐, 𝑏〉)) |
105 | 101, 102,
104 | 3eqtr4g 2681 |
. . . 4
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑐(𝐹 ∘ 𝐷)𝑏) = (𝐹‘(𝑐𝐷𝑏))) |
106 | 97, 105 | oveq12d 6668 |
. . 3
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → ((𝑐(𝐹 ∘ 𝐷)𝑎) +𝑒 (𝑐(𝐹 ∘ 𝐷)𝑏)) = ((𝐹‘(𝑐𝐷𝑎)) +𝑒 (𝐹‘(𝑐𝐷𝑏)))) |
107 | 87, 88, 106 | 3brtr4d 4685 |
. 2
⊢ ((𝜑 ∧ (𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋 ∧ 𝑐 ∈ 𝑋)) → (𝑎(𝐹 ∘ 𝐷)𝑏) ≤ ((𝑐(𝐹 ∘ 𝐷)𝑎) +𝑒 (𝑐(𝐹 ∘ 𝐷)𝑏))) |
108 | 2, 18, 39, 107 | isxmetd 22131 |
1
⊢ (𝜑 → (𝐹 ∘ 𝐷) ∈ (∞Met‘𝑋)) |