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	⊢ 𝐺 = ( toTG ‘ 𝐻 )
	ttgds.1	⊢ 𝐷 = ( dist ‘ 𝐻 )
Assertion	ttgds	⊢ 𝐷 = ( dist ‘ 𝐺 )

Proof

Step	Hyp	Ref	Expression
1		ttgval.n	⊢ 𝐺 = ( toTG ‘ 𝐻 )
2		ttgds.1	⊢ 𝐷 = ( dist ‘ 𝐻 )
3		dsid	⊢ dist = Slot ( dist ‘ ndx )
4		slotslnbpsd	⊢ ( ( ( LineG ‘ ndx ) ≠ ( Base ‘ ndx ) ∧ ( LineG ‘ ndx ) ≠ ( +g ‘ ndx ) ) ∧ ( ( LineG ‘ ndx ) ≠ ( ·𝑠 ‘ ndx ) ∧ ( LineG ‘ ndx ) ≠ ( dist ‘ ndx ) ) )
5		simprr	⊢ ( ( ( ( LineG ‘ ndx ) ≠ ( Base ‘ ndx ) ∧ ( LineG ‘ ndx ) ≠ ( +g ‘ ndx ) ) ∧ ( ( LineG ‘ ndx ) ≠ ( ·𝑠 ‘ 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 ) ≠ ( ·𝑠 ‘ ndx ) ∧ ( Itv ‘ ndx ) ≠ ( dist ‘ ndx ) ) )
9		simprr	⊢ ( ( ( ( Itv ‘ ndx ) ≠ ( Base ‘ ndx ) ∧ ( Itv ‘ ndx ) ≠ ( +g ‘ ndx ) ) ∧ ( ( Itv ‘ ndx ) ≠ ( ·𝑠 ‘ 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 ‘ 𝐻 ) = ( dist ‘ 𝐺 )
13	2 12	eqtri	⊢ 𝐷 = ( dist ‘ 𝐺 )