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 )