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={to𝒢}_{\mathrm{Tarski}}\left(H\right)$$
	ttgds.1	$$⊢D=\mathrm{dist}\left(H\right)$$
Assertion	ttgds	$$⊢D=\mathrm{dist}\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		ttgval.n	$$⊢G={to𝒢}_{\mathrm{Tarski}}\left(H\right)$$
2		ttgds.1	$$⊢D=\mathrm{dist}\left(H\right)$$
3		dsid	$$⊢\mathrm{dist}=\mathrm{Slot}\mathrm{dist}\left(\mathrm{ndx}\right)$$
4		slotslnbpsd	$$⊢\left(\left({Line}_{𝒢}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}\wedge {Line}_{𝒢}\left(\mathrm{ndx}\right)\ne {+}_{\mathrm{ndx}}\right)\wedge \left({Line}_{𝒢}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}\wedge {Line}_{𝒢}\left(\mathrm{ndx}\right)\ne \mathrm{dist}\left(\mathrm{ndx}\right)\right)\right)$$
5		simprr	$$⊢\left(\left({Line}_{𝒢}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}\wedge {Line}_{𝒢}\left(\mathrm{ndx}\right)\ne {+}_{\mathrm{ndx}}\right)\wedge \left({Line}_{𝒢}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}\wedge {Line}_{𝒢}\left(\mathrm{ndx}\right)\ne \mathrm{dist}\left(\mathrm{ndx}\right)\right)\right)\to {Line}_{𝒢}\left(\mathrm{ndx}\right)\ne \mathrm{dist}\left(\mathrm{ndx}\right)$$
6	4 5	ax-mp	$$⊢{Line}_{𝒢}\left(\mathrm{ndx}\right)\ne \mathrm{dist}\left(\mathrm{ndx}\right)$$
7	6	necomi	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\ne {Line}_{𝒢}\left(\mathrm{ndx}\right)$$
8		slotsinbpsd	$$⊢\left(\left(\mathrm{Itv}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}\wedge \mathrm{Itv}\left(\mathrm{ndx}\right)\ne {+}_{\mathrm{ndx}}\right)\wedge \left(\mathrm{Itv}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}\wedge \mathrm{Itv}\left(\mathrm{ndx}\right)\ne \mathrm{dist}\left(\mathrm{ndx}\right)\right)\right)$$
9		simprr	$$⊢\left(\left(\mathrm{Itv}\left(\mathrm{ndx}\right)\ne {\mathrm{Base}}_{\mathrm{ndx}}\wedge \mathrm{Itv}\left(\mathrm{ndx}\right)\ne {+}_{\mathrm{ndx}}\right)\wedge \left(\mathrm{Itv}\left(\mathrm{ndx}\right)\ne {\cdot }_{\mathrm{ndx}}\wedge \mathrm{Itv}\left(\mathrm{ndx}\right)\ne \mathrm{dist}\left(\mathrm{ndx}\right)\right)\right)\to \mathrm{Itv}\left(\mathrm{ndx}\right)\ne \mathrm{dist}\left(\mathrm{ndx}\right)$$
10	8 9	ax-mp	$$⊢\mathrm{Itv}\left(\mathrm{ndx}\right)\ne \mathrm{dist}\left(\mathrm{ndx}\right)$$
11	10	necomi	$$⊢\mathrm{dist}\left(\mathrm{ndx}\right)\ne \mathrm{Itv}\left(\mathrm{ndx}\right)$$
12	1 3 7 11	ttglem	$$⊢\mathrm{dist}\left(H\right)=\mathrm{dist}\left(G\right)$$
13	2 12	eqtri	$$⊢D=\mathrm{dist}\left(G\right)$$