Metamath Proof Explorer

Theorem tmsms

Description: The constructed metric space is a metric space given a metric. (Contributed by Mario Carneiro, 2-Sep-2015)

Ref Expression
Hypothesis tmsbas.k ⊢ K = toMetSp ⁡ D
Assertion tmsms ⊢ D ∈ Met ⁡ X → K ∈ MetSp

Proof

Step Hyp Ref Expression
1 tmsbas.k ⊢ K = toMetSp ⁡ D
2 metxmet ⊢ D ∈ Met ⁡ X → D ∈ ∞Met ⁡ X
3 1 tmsxms ⊢ D ∈ ∞Met ⁡ X → K ∈ ∞MetSp
4 2 3 syl ⊢ D ∈ Met ⁡ X → K ∈ ∞MetSp
5 1 tmsds ⊢ D ∈ ∞Met ⁡ X → D = dist ⁡ K
6 2 5 syl ⊢ D ∈ Met ⁡ X → D = dist ⁡ K
7 1 tmsbas ⊢ D ∈ ∞Met ⁡ X → X = Base K
8 2 7 syl ⊢ D ∈ Met ⁡ X → X = Base K
9 8 fveq2d ⊢ D ∈ Met ⁡ X → Met ⁡ X = Met ⁡ Base K
10 6 9 eleq12d ⊢ D ∈ Met ⁡ X → D ∈ Met ⁡ X ↔ dist ⁡ K ∈ Met ⁡ Base K
11 10 ibi ⊢ D ∈ Met ⁡ X → dist ⁡ K ∈ Met ⁡ Base K
12 ssid ⊢ Base K ⊆ Base K
13 metres2 ⊢ dist ⁡ K ∈ Met ⁡ Base K ∧ Base K ⊆ Base K → dist ⁡ K ↾ Base K × Base K ∈ Met ⁡ Base K
14 11 12 13 sylancl ⊢ D ∈ Met ⁡ X → dist ⁡ K ↾ Base K × Base K ∈ Met ⁡ Base K
15 eqid ⊢ TopOpen ⁡ K = TopOpen ⁡ K
16 eqid ⊢ Base K = Base K
17 eqid ⊢ dist ⁡ K ↾ Base K × Base K = dist ⁡ K ↾ Base K × Base K
18 15 16 17 isms ⊢ K ∈ MetSp ↔ K ∈ ∞MetSp ∧ dist ⁡ K ↾ Base K × Base K ∈ Met ⁡ Base K
19 4 14 18 sylanbrc ⊢ D ∈ Met ⁡ X → K ∈ MetSp