Description: The distance of a pre-Hilbert space augmented with norm. (Contributed by Thierry Arnoux, 30-Jun-2019)
Ref | Expression | ||
---|---|---|---|
Hypotheses | tcphval.n | |
|
tcphds.n | |
||
tcphds.m | |
||
Assertion | tcphds | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | tcphval.n | |
|
2 | tcphds.n | |
|
3 | tcphds.m | |
|
4 | eqid | |
|
5 | eqid | |
|
6 | 1 2 4 5 | tchnmfval | |
7 | 6 | coeq1d | |
8 | 4 | tcphex | |
9 | 1 4 5 | tcphval | |
10 | 9 3 | tngds | |
11 | 8 10 | ax-mp | |
12 | 7 11 | eqtrdi | |