Proof of Theorem metideq
| Step | Hyp | Ref
| Expression |
| 1 | | simpl 482 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → 𝐷 ∈ (PsMet‘𝑋)) |
| 2 | | metidss 33890 |
. . . . . . . . 9
⊢ (𝐷 ∈ (PsMet‘𝑋) →
(~Met‘𝐷)
⊆ (𝑋 × 𝑋)) |
| 3 | | dmss 5913 |
. . . . . . . . 9
⊢
((~Met‘𝐷) ⊆ (𝑋 × 𝑋) → dom (~Met‘𝐷) ⊆ dom (𝑋 × 𝑋)) |
| 4 | 2, 3 | syl 17 |
. . . . . . . 8
⊢ (𝐷 ∈ (PsMet‘𝑋) → dom
(~Met‘𝐷)
⊆ dom (𝑋 ×
𝑋)) |
| 5 | | dmxpid 5941 |
. . . . . . . 8
⊢ dom
(𝑋 × 𝑋) = 𝑋 |
| 6 | 4, 5 | sseqtrdi 4024 |
. . . . . . 7
⊢ (𝐷 ∈ (PsMet‘𝑋) → dom
(~Met‘𝐷)
⊆ 𝑋) |
| 7 | 1, 6 | syl 17 |
. . . . . 6
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → dom (~Met‘𝐷) ⊆ 𝑋) |
| 8 | | xpss 5701 |
. . . . . . . . . 10
⊢ (𝑋 × 𝑋) ⊆ (V × V) |
| 9 | 2, 8 | sstrdi 3996 |
. . . . . . . . 9
⊢ (𝐷 ∈ (PsMet‘𝑋) →
(~Met‘𝐷)
⊆ (V × V)) |
| 10 | | df-rel 5692 |
. . . . . . . . 9
⊢ (Rel
(~Met‘𝐷)
↔ (~Met‘𝐷) ⊆ (V × V)) |
| 11 | 9, 10 | sylibr 234 |
. . . . . . . 8
⊢ (𝐷 ∈ (PsMet‘𝑋) → Rel
(~Met‘𝐷)) |
| 12 | 1, 11 | syl 17 |
. . . . . . 7
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → Rel (~Met‘𝐷)) |
| 13 | | simprl 771 |
. . . . . . 7
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → 𝐴(~Met‘𝐷)𝐵) |
| 14 | | releldm 5955 |
. . . . . . 7
⊢ ((Rel
(~Met‘𝐷)
∧ 𝐴(~Met‘𝐷)𝐵) → 𝐴 ∈ dom (~Met‘𝐷)) |
| 15 | 12, 13, 14 | syl2anc 584 |
. . . . . 6
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → 𝐴 ∈ dom (~Met‘𝐷)) |
| 16 | 7, 15 | sseldd 3984 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → 𝐴 ∈ 𝑋) |
| 17 | | simprr 773 |
. . . . . . 7
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → 𝐸(~Met‘𝐷)𝐹) |
| 18 | | releldm 5955 |
. . . . . . 7
⊢ ((Rel
(~Met‘𝐷)
∧ 𝐸(~Met‘𝐷)𝐹) → 𝐸 ∈ dom (~Met‘𝐷)) |
| 19 | 12, 17, 18 | syl2anc 584 |
. . . . . 6
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → 𝐸 ∈ dom (~Met‘𝐷)) |
| 20 | 7, 19 | sseldd 3984 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → 𝐸 ∈ 𝑋) |
| 21 | | psmetsym 24320 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐸 ∈ 𝑋) → (𝐴𝐷𝐸) = (𝐸𝐷𝐴)) |
| 22 | 1, 16, 20, 21 | syl3anc 1373 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (𝐴𝐷𝐸) = (𝐸𝐷𝐴)) |
| 23 | | psmetf 24316 |
. . . . . 6
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*) |
| 24 | 23 | fovcdmda 7604 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐸 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋)) → (𝐸𝐷𝐴) ∈
ℝ*) |
| 25 | 1, 20, 16, 24 | syl12anc 837 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (𝐸𝐷𝐴) ∈
ℝ*) |
| 26 | 22, 25 | eqeltrd 2841 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (𝐴𝐷𝐸) ∈
ℝ*) |
| 27 | | rnss 5950 |
. . . . . . . 8
⊢
((~Met‘𝐷) ⊆ (𝑋 × 𝑋) → ran (~Met‘𝐷) ⊆ ran (𝑋 × 𝑋)) |
| 28 | 2, 27 | syl 17 |
. . . . . . 7
⊢ (𝐷 ∈ (PsMet‘𝑋) → ran
(~Met‘𝐷)
⊆ ran (𝑋 ×
𝑋)) |
| 29 | | rnxpid 6193 |
. . . . . . 7
⊢ ran
(𝑋 × 𝑋) = 𝑋 |
| 30 | 28, 29 | sseqtrdi 4024 |
. . . . . 6
⊢ (𝐷 ∈ (PsMet‘𝑋) → ran
(~Met‘𝐷)
⊆ 𝑋) |
| 31 | 1, 30 | syl 17 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → ran (~Met‘𝐷) ⊆ 𝑋) |
| 32 | | relelrn 5956 |
. . . . . 6
⊢ ((Rel
(~Met‘𝐷)
∧ 𝐴(~Met‘𝐷)𝐵) → 𝐵 ∈ ran (~Met‘𝐷)) |
| 33 | 12, 13, 32 | syl2anc 584 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → 𝐵 ∈ ran (~Met‘𝐷)) |
| 34 | 31, 33 | sseldd 3984 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → 𝐵 ∈ 𝑋) |
| 35 | 23 | fovcdmda 7604 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐵 ∈ 𝑋 ∧ 𝐸 ∈ 𝑋)) → (𝐵𝐷𝐸) ∈
ℝ*) |
| 36 | 1, 34, 20, 35 | syl12anc 837 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (𝐵𝐷𝐸) ∈
ℝ*) |
| 37 | | relelrn 5956 |
. . . . . . 7
⊢ ((Rel
(~Met‘𝐷)
∧ 𝐸(~Met‘𝐷)𝐹) → 𝐹 ∈ ran (~Met‘𝐷)) |
| 38 | 12, 17, 37 | syl2anc 584 |
. . . . . 6
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → 𝐹 ∈ ran (~Met‘𝐷)) |
| 39 | 31, 38 | sseldd 3984 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → 𝐹 ∈ 𝑋) |
| 40 | | psmetsym 24320 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐹 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐹𝐷𝐵) = (𝐵𝐷𝐹)) |
| 41 | 1, 39, 34, 40 | syl3anc 1373 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (𝐹𝐷𝐵) = (𝐵𝐷𝐹)) |
| 42 | 23 | fovcdmda 7604 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐹 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐹𝐷𝐵) ∈
ℝ*) |
| 43 | 1, 39, 34, 42 | syl12anc 837 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (𝐹𝐷𝐵) ∈
ℝ*) |
| 44 | 41, 43 | eqeltrrd 2842 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (𝐵𝐷𝐹) ∈
ℝ*) |
| 45 | | psmettri2 24319 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐵 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐸 ∈ 𝑋)) → (𝐴𝐷𝐸) ≤ ((𝐵𝐷𝐴) +𝑒 (𝐵𝐷𝐸))) |
| 46 | 1, 34, 16, 20, 45 | syl13anc 1374 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (𝐴𝐷𝐸) ≤ ((𝐵𝐷𝐴) +𝑒 (𝐵𝐷𝐸))) |
| 47 | | psmetsym 24320 |
. . . . . . . 8
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴)) |
| 48 | 1, 16, 34, 47 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (𝐴𝐷𝐵) = (𝐵𝐷𝐴)) |
| 49 | 16, 34 | jca 511 |
. . . . . . . 8
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) |
| 50 | | metidv 33891 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝐴(~Met‘𝐷)𝐵 ↔ (𝐴𝐷𝐵) = 0)) |
| 51 | 50 | biimpa 476 |
. . . . . . . 8
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) ∧ 𝐴(~Met‘𝐷)𝐵) → (𝐴𝐷𝐵) = 0) |
| 52 | 1, 49, 13, 51 | syl21anc 838 |
. . . . . . 7
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (𝐴𝐷𝐵) = 0) |
| 53 | 48, 52 | eqtr3d 2779 |
. . . . . 6
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (𝐵𝐷𝐴) = 0) |
| 54 | 53 | oveq1d 7446 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → ((𝐵𝐷𝐴) +𝑒 (𝐵𝐷𝐸)) = (0 +𝑒 (𝐵𝐷𝐸))) |
| 55 | | xaddlid 13284 |
. . . . . 6
⊢ ((𝐵𝐷𝐸) ∈ ℝ* → (0
+𝑒 (𝐵𝐷𝐸)) = (𝐵𝐷𝐸)) |
| 56 | 36, 55 | syl 17 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (0 +𝑒 (𝐵𝐷𝐸)) = (𝐵𝐷𝐸)) |
| 57 | 54, 56 | eqtrd 2777 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → ((𝐵𝐷𝐴) +𝑒 (𝐵𝐷𝐸)) = (𝐵𝐷𝐸)) |
| 58 | 46, 57 | breqtrd 5169 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (𝐴𝐷𝐸) ≤ (𝐵𝐷𝐸)) |
| 59 | | psmettri2 24319 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐹 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐸 ∈ 𝑋)) → (𝐵𝐷𝐸) ≤ ((𝐹𝐷𝐵) +𝑒 (𝐹𝐷𝐸))) |
| 60 | 1, 39, 34, 20, 59 | syl13anc 1374 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (𝐵𝐷𝐸) ≤ ((𝐹𝐷𝐵) +𝑒 (𝐹𝐷𝐸))) |
| 61 | | psmetsym 24320 |
. . . . . . . 8
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝐹 ∈ 𝑋 ∧ 𝐸 ∈ 𝑋) → (𝐹𝐷𝐸) = (𝐸𝐷𝐹)) |
| 62 | 1, 39, 20, 61 | syl3anc 1373 |
. . . . . . 7
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (𝐹𝐷𝐸) = (𝐸𝐷𝐹)) |
| 63 | 20, 39 | jca 511 |
. . . . . . . 8
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (𝐸 ∈ 𝑋 ∧ 𝐹 ∈ 𝑋)) |
| 64 | | metidv 33891 |
. . . . . . . . 9
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐸 ∈ 𝑋 ∧ 𝐹 ∈ 𝑋)) → (𝐸(~Met‘𝐷)𝐹 ↔ (𝐸𝐷𝐹) = 0)) |
| 65 | 64 | biimpa 476 |
. . . . . . . 8
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐸 ∈ 𝑋 ∧ 𝐹 ∈ 𝑋)) ∧ 𝐸(~Met‘𝐷)𝐹) → (𝐸𝐷𝐹) = 0) |
| 66 | 1, 63, 17, 65 | syl21anc 838 |
. . . . . . 7
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (𝐸𝐷𝐹) = 0) |
| 67 | 62, 66 | eqtrd 2777 |
. . . . . 6
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (𝐹𝐷𝐸) = 0) |
| 68 | 67 | oveq2d 7447 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → ((𝐹𝐷𝐵) +𝑒 (𝐹𝐷𝐸)) = ((𝐹𝐷𝐵) +𝑒 0)) |
| 69 | | xaddrid 13283 |
. . . . . 6
⊢ ((𝐹𝐷𝐵) ∈ ℝ* → ((𝐹𝐷𝐵) +𝑒 0) = (𝐹𝐷𝐵)) |
| 70 | 43, 69 | syl 17 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → ((𝐹𝐷𝐵) +𝑒 0) = (𝐹𝐷𝐵)) |
| 71 | 68, 70, 41 | 3eqtrd 2781 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → ((𝐹𝐷𝐵) +𝑒 (𝐹𝐷𝐸)) = (𝐵𝐷𝐹)) |
| 72 | 60, 71 | breqtrd 5169 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (𝐵𝐷𝐸) ≤ (𝐵𝐷𝐹)) |
| 73 | 26, 36, 44, 58, 72 | xrletrd 13204 |
. 2
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (𝐴𝐷𝐸) ≤ (𝐵𝐷𝐹)) |
| 74 | 23 | fovcdmda 7604 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐹 ∈ 𝑋)) → (𝐴𝐷𝐹) ∈
ℝ*) |
| 75 | 1, 16, 39, 74 | syl12anc 837 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (𝐴𝐷𝐹) ∈
ℝ*) |
| 76 | | psmettri2 24319 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐹 ∈ 𝑋)) → (𝐵𝐷𝐹) ≤ ((𝐴𝐷𝐵) +𝑒 (𝐴𝐷𝐹))) |
| 77 | 1, 16, 34, 39, 76 | syl13anc 1374 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (𝐵𝐷𝐹) ≤ ((𝐴𝐷𝐵) +𝑒 (𝐴𝐷𝐹))) |
| 78 | 52 | oveq1d 7446 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → ((𝐴𝐷𝐵) +𝑒 (𝐴𝐷𝐹)) = (0 +𝑒 (𝐴𝐷𝐹))) |
| 79 | | xaddlid 13284 |
. . . . . 6
⊢ ((𝐴𝐷𝐹) ∈ ℝ* → (0
+𝑒 (𝐴𝐷𝐹)) = (𝐴𝐷𝐹)) |
| 80 | 75, 79 | syl 17 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (0 +𝑒 (𝐴𝐷𝐹)) = (𝐴𝐷𝐹)) |
| 81 | 78, 80 | eqtrd 2777 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → ((𝐴𝐷𝐵) +𝑒 (𝐴𝐷𝐹)) = (𝐴𝐷𝐹)) |
| 82 | 77, 81 | breqtrd 5169 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (𝐵𝐷𝐹) ≤ (𝐴𝐷𝐹)) |
| 83 | | psmettri2 24319 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐸 ∈ 𝑋 ∧ 𝐴 ∈ 𝑋 ∧ 𝐹 ∈ 𝑋)) → (𝐴𝐷𝐹) ≤ ((𝐸𝐷𝐴) +𝑒 (𝐸𝐷𝐹))) |
| 84 | 1, 20, 16, 39, 83 | syl13anc 1374 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (𝐴𝐷𝐹) ≤ ((𝐸𝐷𝐴) +𝑒 (𝐸𝐷𝐹))) |
| 85 | | xaddrid 13283 |
. . . . . 6
⊢ ((𝐸𝐷𝐴) ∈ ℝ* → ((𝐸𝐷𝐴) +𝑒 0) = (𝐸𝐷𝐴)) |
| 86 | 25, 85 | syl 17 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → ((𝐸𝐷𝐴) +𝑒 0) = (𝐸𝐷𝐴)) |
| 87 | 66 | oveq2d 7447 |
. . . . 5
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → ((𝐸𝐷𝐴) +𝑒 (𝐸𝐷𝐹)) = ((𝐸𝐷𝐴) +𝑒 0)) |
| 88 | 86, 87, 22 | 3eqtr4d 2787 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → ((𝐸𝐷𝐴) +𝑒 (𝐸𝐷𝐹)) = (𝐴𝐷𝐸)) |
| 89 | 84, 88 | breqtrd 5169 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (𝐴𝐷𝐹) ≤ (𝐴𝐷𝐸)) |
| 90 | 44, 75, 26, 82, 89 | xrletrd 13204 |
. 2
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (𝐵𝐷𝐹) ≤ (𝐴𝐷𝐸)) |
| 91 | | xrletri3 13196 |
. . 3
⊢ (((𝐴𝐷𝐸) ∈ ℝ* ∧ (𝐵𝐷𝐹) ∈ ℝ*) → ((𝐴𝐷𝐸) = (𝐵𝐷𝐹) ↔ ((𝐴𝐷𝐸) ≤ (𝐵𝐷𝐹) ∧ (𝐵𝐷𝐹) ≤ (𝐴𝐷𝐸)))) |
| 92 | 26, 44, 91 | syl2anc 584 |
. 2
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → ((𝐴𝐷𝐸) = (𝐵𝐷𝐹) ↔ ((𝐴𝐷𝐸) ≤ (𝐵𝐷𝐹) ∧ (𝐵𝐷𝐹) ≤ (𝐴𝐷𝐸)))) |
| 93 | 73, 90, 92 | mpbir2and 713 |
1
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝐴(~Met‘𝐷)𝐵 ∧ 𝐸(~Met‘𝐷)𝐹)) → (𝐴𝐷𝐸) = (𝐵𝐷𝐹)) |