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 | |
|
nmsq.h | |
||
nmsq.n | |
||
Assertion | cphnmfval | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | nmsq.v | |
|
2 | nmsq.h | |
|
3 | nmsq.n | |
|
4 | eqid | |
|
5 | eqid | |
|
6 | 1 2 3 4 5 | iscph | |
7 | 6 | simp3bi | |