Theorem cphtcphnm

Description: The norm of a norm-augmented subcomplex pre-Hilbert space is the same as the original norm on it. (Contributed by Mario Carneiro, 11-Oct-2015)

	Ref	Expression
Hypotheses	tcphval.n	$$⊢G=\mathrm{toCPreHil}\left(W\right)$$
	cphtcphnm.n	$$⊢N=\mathrm{norm}\left(W\right)$$
Assertion	cphtcphnm	$$⊢W\in \mathrm{CPreHil}\to N=\mathrm{norm}\left(G\right)$$

Proof

Step	Hyp	Ref	Expression
1		tcphval.n	$$⊢G=\mathrm{toCPreHil}\left(W\right)$$
2		cphtcphnm.n	$$⊢N=\mathrm{norm}\left(W\right)$$
3		eqid	$$⊢{\mathrm{Base}}_W={\mathrm{Base}}_W$$
4		eqid	$$⊢{\cdot }_{𝑖}\left(W\right)={\cdot }_{𝑖}\left(W\right)$$
5	3 4 2	cphnmfval	$$⊢W\in \mathrm{CPreHil}\to N=\left(x\in {\mathrm{Base}}_W⟼\sqrt{x{\cdot }_{𝑖}\left(W\right)x}\right)$$
6		cphlmod	$$⊢W\in \mathrm{CPreHil}\to W\in \mathrm{LMod}$$
7		lmodgrp	$$⊢W\in \mathrm{LMod}\to W\in \mathrm{Grp}$$
8		eqid	$$⊢\mathrm{norm}\left(G\right)=\mathrm{norm}\left(G\right)$$
9	1 8 3 4	tchnmfval	$$⊢W\in \mathrm{Grp}\to \mathrm{norm}\left(G\right)=\left(x\in {\mathrm{Base}}_W⟼\sqrt{x{\cdot }_{𝑖}\left(W\right)x}\right)$$
10	6 7 9	3syl	$$⊢W\in \mathrm{CPreHil}\to \mathrm{norm}\left(G\right)=\left(x\in {\mathrm{Base}}_W⟼\sqrt{x{\cdot }_{𝑖}\left(W\right)x}\right)$$
11	5 10	eqtr4d	$$⊢W\in \mathrm{CPreHil}\to N=\mathrm{norm}\left(G\right)$$