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 ⊢ 𝐺 = ( toℂPreHil ‘ 𝑊 )
cphtcphnm.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
Assertion cphtcphnm ( 𝑊 ∈ ℂPreHil → 𝑁 = ( norm ‘ 𝐺 ) )

Proof

Step Hyp Ref Expression
1 tcphval.n ⊢ 𝐺 = ( toℂPreHil ‘ 𝑊 )
2 cphtcphnm.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
3 eqid ⊢ ( Base ‘ 𝑊 ) = ( Base ‘ 𝑊 )
4 eqid ⊢ ( ·𝑖 ‘ 𝑊 ) = ( ·𝑖 ‘ 𝑊 )
5 3 4 2 cphnmfval ⊢ ( 𝑊 ∈ ℂPreHil → 𝑁 = ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) ) ) )
6 cphlmod ⊢ ( 𝑊 ∈ ℂPreHil → 𝑊 ∈ LMod )
7 lmodgrp ⊢ ( 𝑊 ∈ LMod → 𝑊 ∈ Grp )
8 eqid ⊢ ( norm ‘ 𝐺 ) = ( norm ‘ 𝐺 )
9 1 8 3 4 tchnmfval ⊢ ( 𝑊 ∈ Grp → ( norm ‘ 𝐺 ) = ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) ) ) )
10 6 7 9 3syl ⊢ ( 𝑊 ∈ ℂPreHil → ( norm ‘ 𝐺 ) = ( 𝑥 ∈ ( Base ‘ 𝑊 ) ↦ ( √ ‘ ( 𝑥 ( ·𝑖 ‘ 𝑊 ) 𝑥 ) ) ) )
11 5 10 eqtr4d ⊢ ( 𝑊 ∈ ℂPreHil → 𝑁 = ( norm ‘ 𝐺 ) )