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

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