Theorem tmsms

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

	Ref	Expression
Hypothesis	tmsbas.k	⊢ 𝐾 = ( toMetSp ‘ 𝐷 )
Assertion	tmsms	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐾 ∈ MetSp )

Proof

Step	Hyp	Ref	Expression
1		tmsbas.k	⊢ 𝐾 = ( toMetSp ‘ 𝐷 )
2		metxmet	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 ∈ ( ∞Met ‘ 𝑋 ) )
3	1	tmsxms	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐾 ∈ ∞MetSp )
4	2 3	syl	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐾 ∈ ∞MetSp )
5	1	tmsds	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 = ( dist ‘ 𝐾 ) )
6	2 5	syl	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐷 = ( dist ‘ 𝐾 ) )
7	1	tmsbas	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝑋 = ( Base ‘ 𝐾 ) )
8	2 7	syl	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝑋 = ( Base ‘ 𝐾 ) )
9	8	fveq2d	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → ( Met ‘ 𝑋 ) = ( Met ‘ ( Base ‘ 𝐾 ) ) )
10	6 9	eleq12d	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → ( 𝐷 ∈ ( Met ‘ 𝑋 ) ↔ ( dist ‘ 𝐾 ) ∈ ( Met ‘ ( Base ‘ 𝐾 ) ) ) )
11	10	ibi	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → ( dist ‘ 𝐾 ) ∈ ( Met ‘ ( Base ‘ 𝐾 ) ) )
12		ssid	⊢ ( Base ‘ 𝐾 ) ⊆ ( Base ‘ 𝐾 )
13		metres2	⊢ ( ( ( dist ‘ 𝐾 ) ∈ ( Met ‘ ( Base ‘ 𝐾 ) ) ∧ ( Base ‘ 𝐾 ) ⊆ ( Base ‘ 𝐾 ) ) → ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ∈ ( Met ‘ ( Base ‘ 𝐾 ) ) )
14	11 12 13	sylancl	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ∈ ( Met ‘ ( Base ‘ 𝐾 ) ) )
15		eqid	⊢ ( TopOpen ‘ 𝐾 ) = ( TopOpen ‘ 𝐾 )
16		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
17		eqid	⊢ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) )
18	15 16 17	isms	⊢ ( 𝐾 ∈ MetSp ↔ ( 𝐾 ∈ ∞MetSp ∧ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ∈ ( Met ‘ ( Base ‘ 𝐾 ) ) ) )
19	4 14 18	sylanbrc	⊢ ( 𝐷 ∈ ( Met ‘ 𝑋 ) → 𝐾 ∈ MetSp )