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

Metamath Proof Explorer

Theorem tcphnmval

Description: The norm of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015)

Ref Expression
Hypotheses tcphval.n ⊢ 𝐺 = ( toℂPreHil ‘ 𝑊 )
tcphnmval.n ⊢ 𝑁 = ( norm ‘ 𝐺 )
tcphnmval.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
tcphnmval.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
Assertion tcphnmval ( ( 𝑊 ∈ Grp ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ 𝑋 ) = ( √ ‘ ( 𝑋 , 𝑋 ) ) )

Proof

Step Hyp Ref Expression
1 tcphval.n ⊢ 𝐺 = ( toℂPreHil ‘ 𝑊 )
2 tcphnmval.n ⊢ 𝑁 = ( norm ‘ 𝐺 )
3 tcphnmval.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
4 tcphnmval.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
5 1 2 3 4 tchnmfval ⊢ ( 𝑊 ∈ Grp → 𝑁 = ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) )
6 5 fveq1d ⊢ ( 𝑊 ∈ Grp → ( 𝑁 ‘ 𝑋 ) = ( ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ‘ 𝑋 ) )
7 oveq12 ⊢ ( ( 𝑥 = 𝑋 ∧ 𝑥 = 𝑋 ) → ( 𝑥 , 𝑥 ) = ( 𝑋 , 𝑋 ) )
8 7 anidms ⊢ ( 𝑥 = 𝑋 → ( 𝑥 , 𝑥 ) = ( 𝑋 , 𝑋 ) )
9 8 fveq2d ⊢ ( 𝑥 = 𝑋 → ( √ ‘ ( 𝑥 , 𝑥 ) ) = ( √ ‘ ( 𝑋 , 𝑋 ) ) )
10 eqid ⊢ ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) = ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) )
11 fvex ⊢ ( √ ‘ ( 𝑋 , 𝑋 ) ) ∈ V
12 9 10 11 fvmpt ⊢ ( 𝑋 ∈ 𝑉 → ( ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ‘ 𝑋 ) = ( √ ‘ ( 𝑋 , 𝑋 ) ) )
13 6 12 sylan9eq ⊢ ( ( 𝑊 ∈ Grp ∧ 𝑋 ∈ 𝑉 ) → ( 𝑁 ‘ 𝑋 ) = ( √ ‘ ( 𝑋 , 𝑋 ) ) )