Theorem setsms

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	|- ( ph -> X = ( Base ` M ) )
	setsms.d	|- ( ph -> D = ( ( dist ` M ) |` ( X X. X ) ) )
	setsms.k	|- ( ph -> K = ( M sSet <. ( TopSet ` ndx ) , ( MetOpen ` D ) >. ) )
	setsms.m	|- ( ph -> M e. V )
Assertion	setsms	|- ( ph -> ( K e. MetSp <-> D e. ( Met ` X ) ) )

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		setsms.m	|- ( ph -> M e. V )
5	1 2 3 4	setsxms	|- ( ph -> ( K e. *MetSp <-> D e. ( *Met ` X ) ) )
6	1 2 3	setsmsds	|- ( ph -> ( dist ` M ) = ( dist ` K ) )
7	1 2 3	setsmsbas	|- ( ph -> X = ( Base ` K ) )
8	7	sqxpeqd	|- ( ph -> ( X X. X ) = ( ( Base ` K ) X. ( Base ` K ) ) )
9	6 8	reseq12d	|- ( ph -> ( ( dist ` M ) |` ( X X. X ) ) = ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) )
10	2 9	eqtr2d	|- ( ph -> ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) = D )
11	7	fveq2d	|- ( ph -> ( Met ` X ) = ( Met ` ( Base ` K ) ) )
12	11	eqcomd	|- ( ph -> ( Met ` ( Base ` K ) ) = ( Met ` X ) )
13	10 12	eleq12d	|- ( ph -> ( ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) e. ( Met ` ( Base ` K ) ) <-> D e. ( Met ` X ) ) )
14	5 13	anbi12d	|- ( ph -> ( ( K e. *MetSp /\ ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) e. ( Met ` ( Base ` K ) ) ) <-> ( D e. ( *Met ` X ) /\ D e. ( Met ` X ) ) ) )
15		eqid	|- ( TopOpen ` K ) = ( TopOpen ` K )
16		eqid	|- ( Base ` K ) = ( Base ` K )
17		eqid	|- ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) = ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) )
18	15 16 17	isms	|- ( K e. MetSp <-> ( K e. *MetSp /\ ( ( dist ` K ) |` ( ( Base ` K ) X. ( Base ` K ) ) ) e. ( Met ` ( Base ` K ) ) ) )
19		metxmet	|- ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
20	19	pm4.71ri	|- ( D e. ( Met ` X ) <-> ( D e. ( *Met ` X ) /\ D e. ( Met ` X ) ) )
21	14 18 20	3bitr4g	|- ( ph -> ( K e. MetSp <-> D e. ( Met ` X ) ) )