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 ⊢ 𝐾 = ( toMetSp ‘ 𝐷 )
Assertion tmsxms ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐾 ∈ ∞MetSp )

Proof

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