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 V=BaseW
nmsq.h ,˙=𝑖W
nmsq.n N=normW
Assertion cphnmfval WCPreHilN=xVx,˙x

Proof

Step Hyp Ref Expression
1 nmsq.v V=BaseW
2 nmsq.h ,˙=𝑖W
3 nmsq.n N=normW
4 eqid ScalarW=ScalarW
5 eqid BaseScalarW=BaseScalarW
6 1 2 3 4 5 iscph WCPreHilWPreHilWNrmModScalarW=fld𝑠BaseScalarWBaseScalarW0+∞BaseScalarWN=xVx,˙x
7 6 simp3bi WCPreHilN=xVx,˙x