Description: Define a function to augment a pre-Hilbert space with a norm. No extra parameters are needed, but some conditions must be satisfied to ensure that this in fact creates a normed subcomplex pre-Hilbert space (see tcphcph ). (Contributed by Mario Carneiro, 7-Oct-2015)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-tcph | |- toCPreHil = ( w e. _V |-> ( w toNrmGrp ( x e. ( Base ` w ) |-> ( sqrt ` ( x ( .i ` w ) x ) ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | ctcph | |- toCPreHil |
|
| 1 | vw | |- w |
|
| 2 | cvv | |- _V |
|
| 3 | 1 | cv | |- w |
| 4 | ctng | |- toNrmGrp |
|
| 5 | vx | |- x |
|
| 6 | cbs | |- Base |
|
| 7 | 3 6 | cfv | |- ( Base ` w ) |
| 8 | csqrt | |- sqrt |
|
| 9 | 5 | cv | |- x |
| 10 | cip | |- .i |
|
| 11 | 3 10 | cfv | |- ( .i ` w ) |
| 12 | 9 9 11 | co | |- ( x ( .i ` w ) x ) |
| 13 | 12 8 | cfv | |- ( sqrt ` ( x ( .i ` w ) x ) ) |
| 14 | 5 7 13 | cmpt | |- ( x e. ( Base ` w ) |-> ( sqrt ` ( x ( .i ` w ) x ) ) ) |
| 15 | 3 14 4 | co | |- ( w toNrmGrp ( x e. ( Base ` w ) |-> ( sqrt ` ( x ( .i ` w ) x ) ) ) ) |
| 16 | 1 2 15 | cmpt | |- ( w e. _V |-> ( w toNrmGrp ( x e. ( Base ` w ) |-> ( sqrt ` ( x ( .i ` w ) x ) ) ) ) ) |
| 17 | 0 16 | wceq | |- toCPreHil = ( w e. _V |-> ( w toNrmGrp ( x e. ( Base ` w ) |-> ( sqrt ` ( x ( .i ` w ) x ) ) ) ) ) |