Proof of Theorem cmspropd
Step | Hyp | Ref
| Expression |
1 | | cmspropd.1 |
. . . 4
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) |
2 | | cmspropd.2 |
. . . 4
⊢ (𝜑 → 𝐵 = (Base‘𝐿)) |
3 | | cmspropd.3 |
. . . 4
⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ (𝐵 × 𝐵))) |
4 | | cmspropd.4 |
. . . 4
⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿)) |
5 | 1, 2, 3, 4 | mspropd 23608 |
. . 3
⊢ (𝜑 → (𝐾 ∈ MetSp ↔ 𝐿 ∈ MetSp)) |
6 | 1 | sqxpeqd 5620 |
. . . . . . 7
⊢ (𝜑 → (𝐵 × 𝐵) = ((Base‘𝐾) × (Base‘𝐾))) |
7 | 6 | reseq2d 5888 |
. . . . . 6
⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾)))) |
8 | 3, 7 | eqtr3d 2781 |
. . . . 5
⊢ (𝜑 → ((dist‘𝐿) ↾ (𝐵 × 𝐵)) = ((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾)))) |
9 | 2 | sqxpeqd 5620 |
. . . . . 6
⊢ (𝜑 → (𝐵 × 𝐵) = ((Base‘𝐿) × (Base‘𝐿))) |
10 | 9 | reseq2d 5888 |
. . . . 5
⊢ (𝜑 → ((dist‘𝐿) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ ((Base‘𝐿) × (Base‘𝐿)))) |
11 | 8, 10 | eqtr3d 2781 |
. . . 4
⊢ (𝜑 → ((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾))) = ((dist‘𝐿) ↾ ((Base‘𝐿) × (Base‘𝐿)))) |
12 | 1, 2 | eqtr3d 2781 |
. . . . 5
⊢ (𝜑 → (Base‘𝐾) = (Base‘𝐿)) |
13 | 12 | fveq2d 6772 |
. . . 4
⊢ (𝜑 →
(CMet‘(Base‘𝐾))
= (CMet‘(Base‘𝐿))) |
14 | 11, 13 | eleq12d 2834 |
. . 3
⊢ (𝜑 → (((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾))) ∈
(CMet‘(Base‘𝐾))
↔ ((dist‘𝐿)
↾ ((Base‘𝐿)
× (Base‘𝐿)))
∈ (CMet‘(Base‘𝐿)))) |
15 | 5, 14 | anbi12d 630 |
. 2
⊢ (𝜑 → ((𝐾 ∈ MetSp ∧ ((dist‘𝐾) ↾ ((Base‘𝐾) × (Base‘𝐾))) ∈
(CMet‘(Base‘𝐾))) ↔ (𝐿 ∈ MetSp ∧ ((dist‘𝐿) ↾ ((Base‘𝐿) × (Base‘𝐿))) ∈
(CMet‘(Base‘𝐿))))) |
16 | | eqid 2739 |
. . 3
⊢
(Base‘𝐾) =
(Base‘𝐾) |
17 | | eqid 2739 |
. . 3
⊢
((dist‘𝐾)
↾ ((Base‘𝐾)
× (Base‘𝐾))) =
((dist‘𝐾) ↾
((Base‘𝐾) ×
(Base‘𝐾))) |
18 | 16, 17 | iscms 24490 |
. 2
⊢ (𝐾 ∈ CMetSp ↔ (𝐾 ∈ MetSp ∧
((dist‘𝐾) ↾
((Base‘𝐾) ×
(Base‘𝐾))) ∈
(CMet‘(Base‘𝐾)))) |
19 | | eqid 2739 |
. . 3
⊢
(Base‘𝐿) =
(Base‘𝐿) |
20 | | eqid 2739 |
. . 3
⊢
((dist‘𝐿)
↾ ((Base‘𝐿)
× (Base‘𝐿))) =
((dist‘𝐿) ↾
((Base‘𝐿) ×
(Base‘𝐿))) |
21 | 19, 20 | iscms 24490 |
. 2
⊢ (𝐿 ∈ CMetSp ↔ (𝐿 ∈ MetSp ∧
((dist‘𝐿) ↾
((Base‘𝐿) ×
(Base‘𝐿))) ∈
(CMet‘(Base‘𝐿)))) |
22 | 15, 18, 21 | 3bitr4g 313 |
1
⊢ (𝜑 → (𝐾 ∈ CMetSp ↔ 𝐿 ∈ CMetSp)) |