Metamath Proof Explorer


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 = toCPreHil W
cphtcphnm.n N = norm W
Assertion cphtcphnm W CPreHil N = norm G

Proof

Step Hyp Ref Expression
1 tcphval.n G = toCPreHil W
2 cphtcphnm.n N = norm W
3 eqid Base W = Base W
4 eqid 𝑖 W = 𝑖 W
5 3 4 2 cphnmfval W CPreHil N = x Base W x 𝑖 W x
6 cphlmod W CPreHil W LMod
7 lmodgrp W LMod W Grp
8 eqid norm G = norm G
9 1 8 3 4 tchnmfval W Grp norm G = x Base W x 𝑖 W x
10 6 7 9 3syl W CPreHil norm G = x Base W x 𝑖 W x
11 5 10 eqtr4d W CPreHil N = norm G