Description: Define the scalar product with a Hilbert space operator. Definition of Beran p. 111. (Contributed by NM, 20-Feb-2006) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-homul | |- .op = ( f e. CC , g e. ( ~H ^m ~H ) |-> ( x e. ~H |-> ( f .h ( g ` x ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | chot | |- .op |
|
| 1 | vf | |- f |
|
| 2 | cc | |- CC |
|
| 3 | vg | |- g |
|
| 4 | chba | |- ~H |
|
| 5 | cmap | |- ^m |
|
| 6 | 4 4 5 | co | |- ( ~H ^m ~H ) |
| 7 | vx | |- x |
|
| 8 | 1 | cv | |- f |
| 9 | csm | |- .h |
|
| 10 | 3 | cv | |- g |
| 11 | 7 | cv | |- x |
| 12 | 11 10 | cfv | |- ( g ` x ) |
| 13 | 8 12 9 | co | |- ( f .h ( g ` x ) ) |
| 14 | 7 4 13 | cmpt | |- ( x e. ~H |-> ( f .h ( g ` x ) ) ) |
| 15 | 1 3 2 6 14 | cmpo | |- ( f e. CC , g e. ( ~H ^m ~H ) |-> ( x e. ~H |-> ( f .h ( g ` x ) ) ) ) |
| 16 | 0 15 | wceq | |- .op = ( f e. CC , g e. ( ~H ^m ~H ) |-> ( x e. ~H |-> ( f .h ( g ` x ) ) ) ) |