Metamath Proof Explorer

Theorem setsms

Description: The constructed metric space is a metric space iff the provided distance function is a metric. (Contributed by Mario Carneiro, 28-Aug-2015)

Ref Expression
Hypotheses setsms.x ⊢ φ → X = Base M
setsms.d ⊢ φ → D = dist ⁡ M ↾ X × X
setsms.k ⊢ φ → K = M sSet TopSet ⁡ ndx MetOpen ⁡ D
setsms.m ⊢ φ → M ∈ V
Assertion setsms ⊢ φ → K ∈ MetSp ↔ D ∈ Met ⁡ X

Proof

Step Hyp Ref Expression
1 setsms.x ⊢ φ → X = Base M
2 setsms.d ⊢ φ → D = dist ⁡ M ↾ X × X
3 setsms.k ⊢ φ → K = M sSet TopSet ⁡ ndx MetOpen ⁡ D
4 setsms.m ⊢ φ → M ∈ V
5 1 2 3 4 setsxms ⊢ φ → K ∈ ∞MetSp ↔ D ∈ ∞Met ⁡ X
6 1 2 3 setsmsds ⊢ φ → dist ⁡ M = dist ⁡ K
7 1 2 3 setsmsbas ⊢ φ → X = Base K
8 7 sqxpeqd ⊢ φ → X × X = Base K × Base K
9 6 8 reseq12d ⊢ φ → dist ⁡ M ↾ X × X = dist ⁡ K ↾ Base K × Base K
10 2 9 eqtr2d ⊢ φ → dist ⁡ K ↾ Base K × Base K = D
11 7 fveq2d ⊢ φ → Met ⁡ X = Met ⁡ Base K
12 11 eqcomd ⊢ φ → Met ⁡ Base K = Met ⁡ X
13 10 12 eleq12d ⊢ φ → dist ⁡ K ↾ Base K × Base K ∈ Met ⁡ Base K ↔ D ∈ Met ⁡ X
14 5 13 anbi12d ⊢ φ → K ∈ ∞MetSp ∧ dist ⁡ K ↾ Base K × Base K ∈ Met ⁡ Base K ↔ D ∈ ∞Met ⁡ X ∧ D ∈ Met ⁡ X
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 metxmet ⊢ D ∈ Met ⁡ X → D ∈ ∞Met ⁡ X
20 19 pm4.71ri ⊢ D ∈ Met ⁡ X ↔ D ∈ ∞Met ⁡ X ∧ D ∈ Met ⁡ X
21 14 18 20 3bitr4g ⊢ φ → K ∈ MetSp ↔ D ∈ Met ⁡ X