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