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=toCPreHilW
tcphds.n N=normG
tcphds.m -˙=-W
Assertion tcphds WGrpN-˙=distG

Proof

Step Hyp Ref Expression
1 tcphval.n G=toCPreHilW
2 tcphds.n N=normG
3 tcphds.m -˙=-W
4 eqid BaseW=BaseW
5 eqid 𝑖W=𝑖W
6 1 2 4 5 tchnmfval WGrpN=xBaseWx𝑖Wx
7 6 coeq1d WGrpN-˙=xBaseWx𝑖Wx-˙
8 4 tcphex xBaseWx𝑖WxV
9 1 4 5 tcphval G=WtoNrmGrpxBaseWx𝑖Wx
10 9 3 tngds xBaseWx𝑖WxVxBaseWx𝑖Wx-˙=distG
11 8 10 ax-mp xBaseWx𝑖Wx-˙=distG
12 7 11 eqtrdi WGrpN-˙=distG