Description: The metric of a constructed metric space. (Contributed by Mario Carneiro, 2-Sep-2015)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | tmsbas.k | β’ πΎ = ( toMetSp β π· ) | |
| Assertion | tmsds | β’ ( π· β ( βMet β π ) β π· = ( dist β πΎ ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | tmsbas.k | β’ πΎ = ( toMetSp β π· ) | |
| 2 | eqid | β’ { β¨ ( Base β ndx ) , π β© , β¨ ( dist β ndx ) , π· β© } = { β¨ ( Base β ndx ) , π β© , β¨ ( dist β ndx ) , π· β© } | |
| 3 | 2 1 | tmslem | β’ ( π· β ( βMet β π ) β ( π = ( Base β πΎ ) β§ π· = ( dist β πΎ ) β§ ( MetOpen β π· ) = ( TopOpen β πΎ ) ) ) |
| 4 | 3 | simp2d | β’ ( π· β ( βMet β π ) β π· = ( dist β πΎ ) ) |