Metamath Proof Explorer

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𝒢 Tarski ⁡ H
ttgds.1 ⊢ D = dist ⁡ H
Assertion ttgds ⊢ D = dist ⁡ G

Proof

Step Hyp Ref Expression
1 ttgval.n ⊢ G = to𝒢 Tarski ⁡ H
2 ttgds.1 ⊢ D = dist ⁡ H
3 dsid ⊢ dist = Slot dist ⁡ ndx
4 slotslnbpsd ⊢ Line 𝒢 ⁡ ndx ≠ Base ndx ∧ Line 𝒢 ⁡ ndx ≠ + ndx ∧ Line 𝒢 ⁡ ndx ≠ ⋅ ndx ∧ Line 𝒢 ⁡ ndx ≠ dist ⁡ ndx
5 simprr ⊢ Line 𝒢 ⁡ ndx ≠ Base ndx ∧ Line 𝒢 ⁡ ndx ≠ + ndx ∧ Line 𝒢 ⁡ ndx ≠ ⋅ ndx ∧ Line 𝒢 ⁡ ndx ≠ dist ⁡ ndx → Line 𝒢 ⁡ ndx ≠ dist ⁡ ndx
6 4 5 ax-mp ⊢ Line 𝒢 ⁡ ndx ≠ dist ⁡ ndx
7 6 necomi ⊢ dist ⁡ ndx ≠ Line 𝒢 ⁡ ndx
8 slotsinbpsd ⊢ Itv ⁡ ndx ≠ Base ndx ∧ Itv ⁡ ndx ≠ + ndx ∧ Itv ⁡ ndx ≠ ⋅ ndx ∧ Itv ⁡ ndx ≠ dist ⁡ ndx
9 simprr ⊢ Itv ⁡ ndx ≠ Base ndx ∧ Itv ⁡ ndx ≠ + 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 ⁡ H = dist ⁡ G
13 2 12 eqtri ⊢ D = dist ⁡ G