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 ) )