| Step | Hyp | Ref
| Expression |
| 1 | | psmetf 24316 |
. . . 4
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*) |
| 2 | 1 | adantr 480 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) → 𝐷:(𝑋 × 𝑋)⟶ℝ*) |
| 3 | | simpr 484 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) → 𝑅 ⊆ 𝑋) |
| 4 | | xpss12 5700 |
. . . 4
⊢ ((𝑅 ⊆ 𝑋 ∧ 𝑅 ⊆ 𝑋) → (𝑅 × 𝑅) ⊆ (𝑋 × 𝑋)) |
| 5 | 3, 3, 4 | syl2anc 584 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) → (𝑅 × 𝑅) ⊆ (𝑋 × 𝑋)) |
| 6 | 2, 5 | fssresd 6775 |
. 2
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) → (𝐷 ↾ (𝑅 × 𝑅)):(𝑅 × 𝑅)⟶ℝ*) |
| 7 | | simpr 484 |
. . . . . 6
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) → 𝑎 ∈ 𝑅) |
| 8 | 7, 7 | ovresd 7600 |
. . . . 5
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) → (𝑎(𝐷 ↾ (𝑅 × 𝑅))𝑎) = (𝑎𝐷𝑎)) |
| 9 | | simpll 767 |
. . . . . 6
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) → 𝐷 ∈ (PsMet‘𝑋)) |
| 10 | 3 | sselda 3983 |
. . . . . 6
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) → 𝑎 ∈ 𝑋) |
| 11 | | psmet0 24318 |
. . . . . 6
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑎 ∈ 𝑋) → (𝑎𝐷𝑎) = 0) |
| 12 | 9, 10, 11 | syl2anc 584 |
. . . . 5
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) → (𝑎𝐷𝑎) = 0) |
| 13 | 8, 12 | eqtrd 2777 |
. . . 4
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) → (𝑎(𝐷 ↾ (𝑅 × 𝑅))𝑎) = 0) |
| 14 | 9 | ad2antrr 726 |
. . . . . . . 8
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) ∧ 𝑐 ∈ 𝑅) → 𝐷 ∈ (PsMet‘𝑋)) |
| 15 | 3 | ad2antrr 726 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) → 𝑅 ⊆ 𝑋) |
| 16 | 15 | sselda 3983 |
. . . . . . . 8
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) ∧ 𝑐 ∈ 𝑅) → 𝑐 ∈ 𝑋) |
| 17 | 10 | ad2antrr 726 |
. . . . . . . 8
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) ∧ 𝑐 ∈ 𝑅) → 𝑎 ∈ 𝑋) |
| 18 | 3 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) → 𝑅 ⊆ 𝑋) |
| 19 | 18 | sselda 3983 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) → 𝑏 ∈ 𝑋) |
| 20 | 19 | adantr 480 |
. . . . . . . 8
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) ∧ 𝑐 ∈ 𝑅) → 𝑏 ∈ 𝑋) |
| 21 | | psmettri2 24319 |
. . . . . . . 8
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ (𝑐 ∈ 𝑋 ∧ 𝑎 ∈ 𝑋 ∧ 𝑏 ∈ 𝑋)) → (𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))) |
| 22 | 14, 16, 17, 20, 21 | syl13anc 1374 |
. . . . . . 7
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) ∧ 𝑐 ∈ 𝑅) → (𝑎𝐷𝑏) ≤ ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))) |
| 23 | 7 | adantr 480 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) → 𝑎 ∈ 𝑅) |
| 24 | | simpr 484 |
. . . . . . . . 9
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) → 𝑏 ∈ 𝑅) |
| 25 | 23, 24 | ovresd 7600 |
. . . . . . . 8
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) → (𝑎(𝐷 ↾ (𝑅 × 𝑅))𝑏) = (𝑎𝐷𝑏)) |
| 26 | 25 | adantr 480 |
. . . . . . 7
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) ∧ 𝑐 ∈ 𝑅) → (𝑎(𝐷 ↾ (𝑅 × 𝑅))𝑏) = (𝑎𝐷𝑏)) |
| 27 | | simpr 484 |
. . . . . . . . 9
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) ∧ 𝑐 ∈ 𝑅) → 𝑐 ∈ 𝑅) |
| 28 | 7 | ad2antrr 726 |
. . . . . . . . 9
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) ∧ 𝑐 ∈ 𝑅) → 𝑎 ∈ 𝑅) |
| 29 | 27, 28 | ovresd 7600 |
. . . . . . . 8
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) ∧ 𝑐 ∈ 𝑅) → (𝑐(𝐷 ↾ (𝑅 × 𝑅))𝑎) = (𝑐𝐷𝑎)) |
| 30 | 24 | adantr 480 |
. . . . . . . . 9
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) ∧ 𝑐 ∈ 𝑅) → 𝑏 ∈ 𝑅) |
| 31 | 27, 30 | ovresd 7600 |
. . . . . . . 8
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) ∧ 𝑐 ∈ 𝑅) → (𝑐(𝐷 ↾ (𝑅 × 𝑅))𝑏) = (𝑐𝐷𝑏)) |
| 32 | 29, 31 | oveq12d 7449 |
. . . . . . 7
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) ∧ 𝑐 ∈ 𝑅) → ((𝑐(𝐷 ↾ (𝑅 × 𝑅))𝑎) +𝑒 (𝑐(𝐷 ↾ (𝑅 × 𝑅))𝑏)) = ((𝑐𝐷𝑎) +𝑒 (𝑐𝐷𝑏))) |
| 33 | 22, 26, 32 | 3brtr4d 5175 |
. . . . . 6
⊢
(((((𝐷 ∈
(PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) ∧ 𝑐 ∈ 𝑅) → (𝑎(𝐷 ↾ (𝑅 × 𝑅))𝑏) ≤ ((𝑐(𝐷 ↾ (𝑅 × 𝑅))𝑎) +𝑒 (𝑐(𝐷 ↾ (𝑅 × 𝑅))𝑏))) |
| 34 | 33 | ralrimiva 3146 |
. . . . 5
⊢ ((((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) ∧ 𝑏 ∈ 𝑅) → ∀𝑐 ∈ 𝑅 (𝑎(𝐷 ↾ (𝑅 × 𝑅))𝑏) ≤ ((𝑐(𝐷 ↾ (𝑅 × 𝑅))𝑎) +𝑒 (𝑐(𝐷 ↾ (𝑅 × 𝑅))𝑏))) |
| 35 | 34 | ralrimiva 3146 |
. . . 4
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) → ∀𝑏 ∈ 𝑅 ∀𝑐 ∈ 𝑅 (𝑎(𝐷 ↾ (𝑅 × 𝑅))𝑏) ≤ ((𝑐(𝐷 ↾ (𝑅 × 𝑅))𝑎) +𝑒 (𝑐(𝐷 ↾ (𝑅 × 𝑅))𝑏))) |
| 36 | 13, 35 | jca 511 |
. . 3
⊢ (((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) ∧ 𝑎 ∈ 𝑅) → ((𝑎(𝐷 ↾ (𝑅 × 𝑅))𝑎) = 0 ∧ ∀𝑏 ∈ 𝑅 ∀𝑐 ∈ 𝑅 (𝑎(𝐷 ↾ (𝑅 × 𝑅))𝑏) ≤ ((𝑐(𝐷 ↾ (𝑅 × 𝑅))𝑎) +𝑒 (𝑐(𝐷 ↾ (𝑅 × 𝑅))𝑏)))) |
| 37 | 36 | ralrimiva 3146 |
. 2
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) → ∀𝑎 ∈ 𝑅 ((𝑎(𝐷 ↾ (𝑅 × 𝑅))𝑎) = 0 ∧ ∀𝑏 ∈ 𝑅 ∀𝑐 ∈ 𝑅 (𝑎(𝐷 ↾ (𝑅 × 𝑅))𝑏) ≤ ((𝑐(𝐷 ↾ (𝑅 × 𝑅))𝑎) +𝑒 (𝑐(𝐷 ↾ (𝑅 × 𝑅))𝑏)))) |
| 38 | | elfvex 6944 |
. . . . 5
⊢ (𝐷 ∈ (PsMet‘𝑋) → 𝑋 ∈ V) |
| 39 | 38 | adantr 480 |
. . . 4
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) → 𝑋 ∈ V) |
| 40 | 39, 3 | ssexd 5324 |
. . 3
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) → 𝑅 ∈ V) |
| 41 | | ispsmet 24314 |
. . 3
⊢ (𝑅 ∈ V → ((𝐷 ↾ (𝑅 × 𝑅)) ∈ (PsMet‘𝑅) ↔ ((𝐷 ↾ (𝑅 × 𝑅)):(𝑅 × 𝑅)⟶ℝ* ∧
∀𝑎 ∈ 𝑅 ((𝑎(𝐷 ↾ (𝑅 × 𝑅))𝑎) = 0 ∧ ∀𝑏 ∈ 𝑅 ∀𝑐 ∈ 𝑅 (𝑎(𝐷 ↾ (𝑅 × 𝑅))𝑏) ≤ ((𝑐(𝐷 ↾ (𝑅 × 𝑅))𝑎) +𝑒 (𝑐(𝐷 ↾ (𝑅 × 𝑅))𝑏)))))) |
| 42 | 40, 41 | syl 17 |
. 2
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) → ((𝐷 ↾ (𝑅 × 𝑅)) ∈ (PsMet‘𝑅) ↔ ((𝐷 ↾ (𝑅 × 𝑅)):(𝑅 × 𝑅)⟶ℝ* ∧
∀𝑎 ∈ 𝑅 ((𝑎(𝐷 ↾ (𝑅 × 𝑅))𝑎) = 0 ∧ ∀𝑏 ∈ 𝑅 ∀𝑐 ∈ 𝑅 (𝑎(𝐷 ↾ (𝑅 × 𝑅))𝑏) ≤ ((𝑐(𝐷 ↾ (𝑅 × 𝑅))𝑎) +𝑒 (𝑐(𝐷 ↾ (𝑅 × 𝑅))𝑏)))))) |
| 43 | 6, 37, 42 | mpbir2and 713 |
1
⊢ ((𝐷 ∈ (PsMet‘𝑋) ∧ 𝑅 ⊆ 𝑋) → (𝐷 ↾ (𝑅 × 𝑅)) ∈ (PsMet‘𝑅)) |