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 = ( Base ` W ) |
|
| nmsq.h | |- ., = ( .i ` W ) |
||
| nmsq.n | |- N = ( norm ` W ) |
||
| Assertion | cphnmfval | |- ( W e. CPreHil -> N = ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | nmsq.v | |- V = ( Base ` W ) |
|
| 2 | nmsq.h | |- ., = ( .i ` W ) |
|
| 3 | nmsq.n | |- N = ( norm ` W ) |
|
| 4 | eqid | |- ( Scalar ` W ) = ( Scalar ` W ) |
|
| 5 | eqid | |- ( Base ` ( Scalar ` W ) ) = ( Base ` ( Scalar ` W ) ) |
|
| 6 | 1 2 3 4 5 | iscph | |- ( W e. CPreHil <-> ( ( W e. PreHil /\ W e. NrmMod /\ ( Scalar ` W ) = ( CCfld |`s ( Base ` ( Scalar ` W ) ) ) ) /\ ( sqrt " ( ( Base ` ( Scalar ` W ) ) i^i ( 0 [,) +oo ) ) ) C_ ( Base ` ( Scalar ` W ) ) /\ N = ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ) ) |
| 7 | 6 | simp3bi | |- ( W e. CPreHil -> N = ( x e. V |-> ( sqrt ` ( x ., x ) ) ) ) |