Metamath Proof Explorer

Theorem tmsxms

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

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

Proof

Step Hyp Ref Expression
1 tmsbas.k ⊢ K = toMetSp ⁡ D
2 1 tmsds ⊢ D ∈ ∞Met ⁡ X → D = dist ⁡ K
3 1 tmsbas ⊢ D ∈ ∞Met ⁡ X → X = Base K
4 3 fveq2d ⊢ D ∈ ∞Met ⁡ X → ∞Met ⁡ X = ∞Met ⁡ Base K
5 2 4 eleq12d ⊢ D ∈ ∞Met ⁡ X → D ∈ ∞Met ⁡ X ↔ dist ⁡ K ∈ ∞Met ⁡ Base K
6 5 ibi ⊢ D ∈ ∞Met ⁡ X → dist ⁡ K ∈ ∞Met ⁡ Base K
7 ssid ⊢ Base K ⊆ Base K
8 xmetres2 ⊢ dist ⁡ K ∈ ∞Met ⁡ Base K ∧ Base K ⊆ Base K → dist ⁡ K ↾ Base K × Base K ∈ ∞Met ⁡ Base K
9 6 7 8 sylancl ⊢ D ∈ ∞Met ⁡ X → dist ⁡ K ↾ Base K × Base K ∈ ∞Met ⁡ Base K
10 xmetf ⊢ dist ⁡ K ∈ ∞Met ⁡ Base K → dist ⁡ K : Base K × Base K ⟶ ℝ *
11 ffn ⊢ dist ⁡ K : Base K × Base K ⟶ ℝ * → dist ⁡ K Fn Base K × Base K
12 fnresdm ⊢ dist ⁡ K Fn Base K × Base K → dist ⁡ K ↾ Base K × Base K = dist ⁡ K
13 6 10 11 12 4syl ⊢ D ∈ ∞Met ⁡ X → dist ⁡ K ↾ Base K × Base K = dist ⁡ K
14 13 2 eqtr4d ⊢ D ∈ ∞Met ⁡ X → dist ⁡ K ↾ Base K × Base K = D
15 14 fveq2d ⊢ D ∈ ∞Met ⁡ X → MetOpen ⁡ dist ⁡ K ↾ Base K × Base K = MetOpen ⁡ D
16 eqid ⊢ MetOpen ⁡ D = MetOpen ⁡ D
17 1 16 tmstopn ⊢ D ∈ ∞Met ⁡ X → MetOpen ⁡ D = TopOpen ⁡ K
18 15 17 eqtr2d ⊢ D ∈ ∞Met ⁡ X → TopOpen ⁡ K = MetOpen ⁡ dist ⁡ K ↾ Base K × Base K
19 eqid ⊢ TopOpen ⁡ K = TopOpen ⁡ K
20 eqid ⊢ Base K = Base K
21 eqid ⊢ dist ⁡ K ↾ Base K × Base K = dist ⁡ K ↾ Base K × Base K
22 19 20 21 isxms2 ⊢ K ∈ ∞MetSp ↔ dist ⁡ K ↾ Base K × Base K ∈ ∞Met ⁡ Base K ∧ TopOpen ⁡ K = MetOpen ⁡ dist ⁡ K ↾ Base K × Base K
23 9 18 22 sylanbrc ⊢ D ∈ ∞Met ⁡ X → K ∈ ∞MetSp