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

Metamath Proof Explorer

Theorem cphnmfval

Description: The value of the norm in a subcomplex pre-Hilbert space is the square root of the inner product of a vector with itself. (Contributed by Mario Carneiro, 7-Oct-2015)

Ref Expression
Hypotheses nmsq.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
nmsq.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
nmsq.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
Assertion cphnmfval ( 𝑊 ∈ ℂPreHil → 𝑁 = ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) )

Proof

Step Hyp Ref Expression
1 nmsq.v ⊢ 𝑉 = ( Base ‘ 𝑊 )
2 nmsq.h ⊢ , = ( ·𝑖 ‘ 𝑊 )
3 nmsq.n ⊢ 𝑁 = ( norm ‘ 𝑊 )
4 eqid ⊢ ( Scalar ‘ 𝑊 ) = ( Scalar ‘ 𝑊 )
5 eqid ⊢ ( Base ‘ ( Scalar ‘ 𝑊 ) ) = ( Base ‘ ( Scalar ‘ 𝑊 ) )
6 1 2 3 4 5 iscph ⊢ ( 𝑊 ∈ ℂPreHil ↔ ( ( 𝑊 ∈ PreHil ∧ 𝑊 ∈ NrmMod ∧ ( Scalar ‘ 𝑊 ) = ( ℂfld ↾s ( Base ‘ ( Scalar ‘ 𝑊 ) ) ) ) ∧ ( √ “ ( ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∩ ( 0 [,) +∞ ) ) ) ⊆ ( Base ‘ ( Scalar ‘ 𝑊 ) ) ∧ 𝑁 = ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) ) )
7 6 simp3bi ⊢ ( 𝑊 ∈ ℂPreHil → 𝑁 = ( 𝑥 ∈ 𝑉 ↦ ( √ ‘ ( 𝑥 , 𝑥 ) ) ) )