Theorem ttgds

Description: The metric of a subcomplex Hilbert space augmented with betweenness. (Contributed by Thierry Arnoux, 25-Mar-2019) (Revised by AV, 29-Oct-2024)

	Ref	Expression
Hypotheses	ttgval.n	|- G = ( toTG ` H )
	ttgds.1	|- D = ( dist ` H )
Assertion	ttgds	|- D = ( dist ` G )

Proof

Step	Hyp	Ref	Expression
1		ttgval.n	|- G = ( toTG ` H )
2		ttgds.1	|- D = ( dist ` H )
3		dsid	|- dist = Slot ( dist ` ndx )
4		slotslnbpsd	|- ( ( ( LineG ` ndx ) =/= ( Base ` ndx ) /\ ( LineG ` ndx ) =/= ( +g ` ndx ) ) /\ ( ( LineG ` ndx ) =/= ( .s ` ndx ) /\ ( LineG ` ndx ) =/= ( dist ` ndx ) ) )
5		simprr	|- ( ( ( ( LineG ` ndx ) =/= ( Base ` ndx ) /\ ( LineG ` ndx ) =/= ( +g ` ndx ) ) /\ ( ( LineG ` ndx ) =/= ( .s ` ndx ) /\ ( LineG ` ndx ) =/= ( dist ` ndx ) ) ) -> ( LineG ` ndx ) =/= ( dist ` ndx ) )
6	4 5	ax-mp	|- ( LineG ` ndx ) =/= ( dist ` ndx )
7	6	necomi	|- ( dist ` ndx ) =/= ( LineG ` ndx )
8		slotsinbpsd	|- ( ( ( Itv ` ndx ) =/= ( Base ` ndx ) /\ ( Itv ` ndx ) =/= ( +g ` ndx ) ) /\ ( ( Itv ` ndx ) =/= ( .s ` ndx ) /\ ( Itv ` ndx ) =/= ( dist ` ndx ) ) )
9		simprr	|- ( ( ( ( Itv ` ndx ) =/= ( Base ` ndx ) /\ ( Itv ` ndx ) =/= ( +g ` ndx ) ) /\ ( ( Itv ` ndx ) =/= ( .s ` ndx ) /\ ( Itv ` ndx ) =/= ( dist ` ndx ) ) ) -> ( Itv ` ndx ) =/= ( dist ` ndx ) )
10	8 9	ax-mp	|- ( Itv ` ndx ) =/= ( dist ` ndx )
11	10	necomi	|- ( dist ` ndx ) =/= ( Itv ` ndx )
12	1 3 7 11	ttglem	|- ( dist ` H ) = ( dist ` G )
13	2 12	eqtri	|- D = ( dist ` G )