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=\mathrm{toCPreHil}\left(W\right)$$
	tcphds.n	$$⊢N=\mathrm{norm}\left(G\right)$$
	tcphds.m	$$⊢\underset{\dot{}}{-}={-}_W$$
Assertion	tcphds	$$⊢W\in \mathrm{Grp}\to N\circ \underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		tcphval.n	$$⊢G=\mathrm{toCPreHil}\left(W\right)$$
2		tcphds.n	$$⊢N=\mathrm{norm}\left(G\right)$$
3		tcphds.m	$$⊢\underset{\dot{}}{-}={-}_W$$
4		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
5		eqid	$$⊢{\cdot }_{𝑖}\left(W\right)={\cdot }_{𝑖}\left(W\right)$$
6	1 2 4 5	tchnmfval	$$⊢W\in \mathrm{Grp}\to N=\left(x\in {\mathrm{Base}}_W⟼\sqrt{x{\cdot }_{𝑖}\left(W\right)x}\right)$$
7	6	coeq1d	$$⊢W\in \mathrm{Grp}\to N\circ \underset{\dot{}}{-}=\left(x\in {\mathrm{Base}}_W⟼\sqrt{x{\cdot }_{𝑖}\left(W\right)x}\right)\circ \underset{\dot{}}{-}$$
8	4	tcphex	$$⊢\left(x\in {\mathrm{Base}}_W⟼\sqrt{x{\cdot }_{𝑖}\left(W\right)x}\right)\in \mathrm{V}$$
9	1 4 5	tcphval	$$⊢G=W\mathrm{toNrmGrp}\left(x\in {\mathrm{Base}}_W⟼\sqrt{x{\cdot }_{𝑖}\left(W\right)x}\right)$$
10	9 3	tngds	$$⊢\left(x\in {\mathrm{Base}}_W⟼\sqrt{x{\cdot }_{𝑖}\left(W\right)x}\right)\in \mathrm{V}\to \left(x\in {\mathrm{Base}}_W⟼\sqrt{x{\cdot }_{𝑖}\left(W\right)x}\right)\circ \underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
11	8 10	ax-mp	$$⊢\left(x\in {\mathrm{Base}}_W⟼\sqrt{x{\cdot }_{𝑖}\left(W\right)x}\right)\circ \underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$
12	7 11	syl6eq	$$⊢W\in \mathrm{Grp}\to N\circ \underset{\dot{}}{-}=\mathrm{dist}\left(G\right)$$