Metamath Proof Explorer

Theorem metgt0

Description: The distance function of a metric space is positive for unequal points. Definition 14-1.1(b) of Gleason p. 223 and its converse. (Contributed by NM, 27-Aug-2006)

		Ref	Expression
	Assertion	metgt0	\|- ( ( D e. ( Met ` X ) /\ A e. X /\ B e. X ) -> ( A =/= B <-> 0 < ( A D B ) ) )

Proof

Step	Hyp	Ref	Expression
1		metxmet	\|- ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )
2		xmetgt0	\|- ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( A =/= B <-> 0 < ( A D B ) ) )
3	1 2	syl3an1	\|- ( ( D e. ( Met ` X ) /\ A e. X /\ B e. X ) -> ( A =/= B <-> 0 < ( A D B ) ) )

Step

Hyp

Ref

Expression

metxmet

 |-  ( D e. ( Met ` X ) -> D e. ( *Met ` X ) )

xmetgt0

 |-  ( ( D e. ( *Met ` X ) /\ A e. X /\ B e. X ) -> ( A =/= B <-> 0 < ( A D B ) ) )

1 2

syl3an1

 |-  ( ( D e. ( Met ` X ) /\ A e. X /\ B e. X ) -> ( A =/= B <-> 0 < ( A D B ) ) )