Theorem setsmsds

Description: The distance function of a constructed metric space. (Contributed by Mario Carneiro, 28-Aug-2015) (Proof shortened by AV, 11-Nov-2024)

	Ref	Expression
Hypotheses	setsms.x	|- ( ph -> X = ( Base ` M ) )
	setsms.d	|- ( ph -> D = ( ( dist ` M ) |` ( X X. X ) ) )
	setsms.k	|- ( ph -> K = ( M sSet <. ( TopSet ` ndx ) , ( MetOpen ` D ) >. ) )
Assertion	setsmsds	|- ( ph -> ( dist ` M ) = ( dist ` K ) )

Proof

Step	Hyp	Ref	Expression
1		setsms.x	|- ( ph -> X = ( Base ` M ) )
2		setsms.d	|- ( ph -> D = ( ( dist ` M ) |` ( X X. X ) ) )
3		setsms.k	|- ( ph -> K = ( M sSet <. ( TopSet ` ndx ) , ( MetOpen ` D ) >. ) )
4		dsid	|- dist = Slot ( dist ` ndx )
5		dsndxntsetndx	|- ( dist ` ndx ) =/= ( TopSet ` ndx )
6	4 5	setsnid	|- ( dist ` M ) = ( dist ` ( M sSet <. ( TopSet ` ndx ) , ( MetOpen ` D ) >. ) )
7	3	fveq2d	|- ( ph -> ( dist ` K ) = ( dist ` ( M sSet <. ( TopSet ` ndx ) , ( MetOpen ` D ) >. ) ) )
8	6 7	eqtr4id	|- ( ph -> ( dist ` M ) = ( dist ` K ) )