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 β†’ 𝑁 = ( π‘₯ ∈ 𝑉 ↦ ( √ β€˜ ( π‘₯ , π‘₯ ) ) ) )