Metamath Proof Explorer
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 ‘ 𝐺 ) |