setsxms

Description: The constructed metric space is a metric space iff the provided distance function is a metric. (Contributed by Mario Carneiro, 28-Aug-2015)

	Ref	Expression
Hypotheses	setsms.x	⊢ ( 𝜑 → 𝑋 = ( Base ‘ 𝑀 ) )
	setsms.d	⊢ ( 𝜑 → 𝐷 = ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) )
	setsms.k	⊢ ( 𝜑 → 𝐾 = ( 𝑀 sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ 𝐷 ) ⟩ ) )
	setsms.m	⊢ ( 𝜑 → 𝑀 ∈ 𝑉 )
Assertion	setsxms	⊢ ( 𝜑 → ( 𝐾 ∈ ∞MetSp ↔ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) )

Proof

Step	Hyp	Ref	Expression
1		setsms.x	⊢ ( 𝜑 → 𝑋 = ( Base ‘ 𝑀 ) )
2		setsms.d	⊢ ( 𝜑 → 𝐷 = ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) )
3		setsms.k	⊢ ( 𝜑 → 𝐾 = ( 𝑀 sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ 𝐷 ) ⟩ ) )
4		setsms.m	⊢ ( 𝜑 → 𝑀 ∈ 𝑉 )
5	1 2 3 4	setsmstopn	⊢ ( 𝜑 → ( MetOpen ‘ 𝐷 ) = ( TopOpen ‘ 𝐾 ) )
6	1 2 3	setsmsds	⊢ ( 𝜑 → ( dist ‘ 𝑀 ) = ( dist ‘ 𝐾 ) )
7	1 2 3	setsmsbas	⊢ ( 𝜑 → 𝑋 = ( Base ‘ 𝐾 ) )
8	7	sqxpeqd	⊢ ( 𝜑 → ( 𝑋 × 𝑋 ) = ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) )
9	6 8	reseq12d	⊢ ( 𝜑 → ( ( dist ‘ 𝑀 ) ↾ ( 𝑋 × 𝑋 ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) )
10	2 9	eqtrd	⊢ ( 𝜑 → 𝐷 = ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) )
11	10	fveq2d	⊢ ( 𝜑 → ( MetOpen ‘ 𝐷 ) = ( MetOpen ‘ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ) )
12	5 11	eqtr3d	⊢ ( 𝜑 → ( TopOpen ‘ 𝐾 ) = ( MetOpen ‘ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ) )
13		eqid	⊢ ( TopOpen ‘ 𝐾 ) = ( TopOpen ‘ 𝐾 )
14		eqid	⊢ ( Base ‘ 𝐾 ) = ( Base ‘ 𝐾 )
15		eqid	⊢ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) = ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) )
16	13 14 15	isxms2	⊢ ( 𝐾 ∈ ∞MetSp ↔ ( ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝐾 ) ) ∧ ( TopOpen ‘ 𝐾 ) = ( MetOpen ‘ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ) ) )
17	16	rbaib	⊢ ( ( TopOpen ‘ 𝐾 ) = ( MetOpen ‘ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ) → ( 𝐾 ∈ ∞MetSp ↔ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝐾 ) ) ) )
18	12 17	syl	⊢ ( 𝜑 → ( 𝐾 ∈ ∞MetSp ↔ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝐾 ) ) ) )
19	7	fveq2d	⊢ ( 𝜑 → ( ∞Met ‘ 𝑋 ) = ( ∞Met ‘ ( Base ‘ 𝐾 ) ) )
20	10 19	eleq12d	⊢ ( 𝜑 → ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ↔ ( ( dist ‘ 𝐾 ) ↾ ( ( Base ‘ 𝐾 ) × ( Base ‘ 𝐾 ) ) ) ∈ ( ∞Met ‘ ( Base ‘ 𝐾 ) ) ) )
21	18 20	bitr4d	⊢ ( 𝜑 → ( 𝐾 ∈ ∞MetSp ↔ 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ) )

Metamath Proof Explorer

Theorem setsxms

Proof