Theorem trkgdist

Description: The measure of a distance in a Tarski geometry. (Contributed by Thierry Arnoux, 24-Aug-2017)

	Ref	Expression
Hypothesis	trkgstr.w	|- W = { <. ( Base ` ndx ) , U >. , <. ( dist ` ndx ) , D >. , <. ( Itv ` ndx ) , I >. }
Assertion	trkgdist	|- ( D e. V -> D = ( dist ` W ) )

Proof

Step	Hyp	Ref	Expression
1		trkgstr.w	|- W = { <. ( Base ` ndx ) , U >. , <. ( dist ` ndx ) , D >. , <. ( Itv ` ndx ) , I >. }
2	1	trkgstr	|- W Struct <. 1 , ; 1 6 >.
3		dsid	|- dist = Slot ( dist ` ndx )
4		snsstp2	|- { <. ( dist ` ndx ) , D >. } C_ { <. ( Base ` ndx ) , U >. , <. ( dist ` ndx ) , D >. , <. ( Itv ` ndx ) , I >. }
5	4 1	sseqtrri	|- { <. ( dist ` ndx ) , D >. } C_ W
6	2 3 5	strfv	|- ( D e. V -> D = ( dist ` W ) )