Metamath Proof Explorer


Theorem tcphds

Description: The distance of a pre-Hilbert space augmented with norm. (Contributed by Thierry Arnoux, 30-Jun-2019)

Ref Expression
Hypotheses tcphval.n G = toCPreHil W
tcphds.n N = norm G
tcphds.m - ˙ = - W
Assertion tcphds W Grp N - ˙ = dist G

Proof

Step Hyp Ref Expression
1 tcphval.n G = toCPreHil W
2 tcphds.n N = norm G
3 tcphds.m - ˙ = - W
4 eqid Base W = Base W
5 eqid 𝑖 W = 𝑖 W
6 1 2 4 5 tchnmfval W Grp N = x Base W x 𝑖 W x
7 6 coeq1d W Grp N - ˙ = x Base W x 𝑖 W x - ˙
8 4 tcphex x Base W x 𝑖 W x V
9 1 4 5 tcphval G = W toNrmGrp x Base W x 𝑖 W x
10 9 3 tngds x Base W x 𝑖 W x V x Base W x 𝑖 W x - ˙ = dist G
11 8 10 ax-mp x Base W x 𝑖 W x - ˙ = dist G
12 7 11 eqtrdi W Grp N - ˙ = dist G