This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 
|- .- = ( -g ` W )
Assertion tcphds 
|- ( W e. Grp -> ( N o. .- ) = ( dist ` G ) )

Proof

Step Hyp Ref Expression
1 tcphval.n 
 |-  G = ( toCPreHil ` W )
2 tcphds.n 
 |-  N = ( norm ` G )
3 tcphds.m 
 |-  .- = ( -g ` W )
4 eqid 
 |-  ( Base ` W ) = ( Base ` W )
5 eqid 
 |-  ( .i ` W ) = ( .i ` W )
6 1 2 4 5 tchnmfval 
 |-  ( W e. Grp -> N = ( x e. ( Base ` W ) |-> ( sqrt ` ( x ( .i ` W ) x ) ) ) )
7 6 coeq1d 
 |-  ( W e. Grp -> ( N o. .- ) = ( ( x e. ( Base ` W ) |-> ( sqrt ` ( x ( .i ` W ) x ) ) ) o. .- ) )
8 4 tcphex 
 |-  ( x e. ( Base ` W ) |-> ( sqrt ` ( x ( .i ` W ) x ) ) ) e. _V
9 1 4 5 tcphval 
 |-  G = ( W toNrmGrp ( x e. ( Base ` W ) |-> ( sqrt ` ( x ( .i ` W ) x ) ) ) )
10 9 3 tngds 
 |-  ( ( x e. ( Base ` W ) |-> ( sqrt ` ( x ( .i ` W ) x ) ) ) e. _V -> ( ( x e. ( Base ` W ) |-> ( sqrt ` ( x ( .i ` W ) x ) ) ) o. .- ) = ( dist ` G ) )
11 8 10 ax-mp 
 |-  ( ( x e. ( Base ` W ) |-> ( sqrt ` ( x ( .i ` W ) x ) ) ) o. .- ) = ( dist ` G )
12 7 11 eqtrdi 
 |-  ( W e. Grp -> ( N o. .- ) = ( dist ` G ) )