Metamath Proof Explorer


Theorem ttgds

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

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 df-ds dist = Slot 1 2
4 1nn0 1 ∈ ℕ0
5 2nn 2 ∈ ℕ
6 4 5 decnncl 1 2 ∈ ℕ
7 2nn0 2 ∈ ℕ0
8 6nn 6 ∈ ℕ
9 2lt6 2 < 6
10 4 7 8 9 declt 1 2 < 1 6
11 1 3 6 10 ttglem ( dist ‘ 𝐻 ) = ( dist ‘ 𝐺 )
12 2 11 eqtri 𝐷 = ( dist ‘ 𝐺 )