tmsval

Description: For any metric there is an associated metric space. (Contributed by Mario Carneiro, 2-Sep-2015)

	Ref	Expression
Hypotheses	tmsval.m	⊢ 𝑀 = { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ }
	tmsval.k	⊢ 𝐾 = ( toMetSp ‘ 𝐷 )
Assertion	tmsval	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐾 = ( 𝑀 sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ 𝐷 ) ⟩ ) )

Proof

Step	Hyp	Ref	Expression
1		tmsval.m	⊢ 𝑀 = { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ }
2		tmsval.k	⊢ 𝐾 = ( toMetSp ‘ 𝐷 )
3		df-tms	⊢ toMetSp = ( 𝑑 ∈ ∪ ran ∞Met ↦ ( { ⟨ ( Base ‘ ndx ) , dom dom 𝑑 ⟩ , ⟨ ( dist ‘ ndx ) , 𝑑 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ 𝑑 ) ⟩ ) )
4		dmeq	⊢ ( 𝑑 = 𝐷 → dom 𝑑 = dom 𝐷 )
5	4	dmeqd	⊢ ( 𝑑 = 𝐷 → dom dom 𝑑 = dom dom 𝐷 )
6		xmetf	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 : ( 𝑋 × 𝑋 ) ⟶ ℝ^* )
7	6	fdmd	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → dom 𝐷 = ( 𝑋 × 𝑋 ) )
8	7	dmeqd	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → dom dom 𝐷 = dom ( 𝑋 × 𝑋 ) )
9		dmxpid	⊢ dom ( 𝑋 × 𝑋 ) = 𝑋
10	8 9	eqtrdi	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → dom dom 𝐷 = 𝑋 )
11	5 10	sylan9eqr	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → dom dom 𝑑 = 𝑋 )
12	11	opeq2d	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ⟨ ( Base ‘ ndx ) , dom dom 𝑑 ⟩ = ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ )
13		simpr	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → 𝑑 = 𝐷 )
14	13	opeq2d	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ⟨ ( dist ‘ ndx ) , 𝑑 ⟩ = ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ )
15	12 14	preq12d	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → { ⟨ ( Base ‘ ndx ) , dom dom 𝑑 ⟩ , ⟨ ( dist ‘ ndx ) , 𝑑 ⟩ } = { ⟨ ( Base ‘ ndx ) , 𝑋 ⟩ , ⟨ ( dist ‘ ndx ) , 𝐷 ⟩ } )
16	15 1	eqtr4di	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → { ⟨ ( Base ‘ ndx ) , dom dom 𝑑 ⟩ , ⟨ ( dist ‘ ndx ) , 𝑑 ⟩ } = 𝑀 )
17	13	fveq2d	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( MetOpen ‘ 𝑑 ) = ( MetOpen ‘ 𝐷 ) )
18	17	opeq2d	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ 𝑑 ) ⟩ = ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ 𝐷 ) ⟩ )
19	16 18	oveq12d	⊢ ( ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) ∧ 𝑑 = 𝐷 ) → ( { ⟨ ( Base ‘ ndx ) , dom dom 𝑑 ⟩ , ⟨ ( dist ‘ ndx ) , 𝑑 ⟩ } sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ 𝑑 ) ⟩ ) = ( 𝑀 sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ 𝐷 ) ⟩ ) )
20		fvssunirn	⊢ ( ∞Met ‘ 𝑋 ) ⊆ ∪ ran ∞Met
21	20	sseli	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐷 ∈ ∪ ran ∞Met )
22		ovexd	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( 𝑀 sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ 𝐷 ) ⟩ ) ∈ V )
23	3 19 21 22	fvmptd2	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → ( toMetSp ‘ 𝐷 ) = ( 𝑀 sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ 𝐷 ) ⟩ ) )
24	2 23	eqtrid	⊢ ( 𝐷 ∈ ( ∞Met ‘ 𝑋 ) → 𝐾 = ( 𝑀 sSet ⟨ ( TopSet ‘ ndx ) , ( MetOpen ‘ 𝐷 ) ⟩ ) )

Metamath Proof Explorer

Theorem tmsval

Proof