Description: Define the scalar product with a Hilbert space functional. Definition of Beran p. 111. (Contributed by NM, 23-May-2006) (New usage is discouraged.)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-hfmul | ⊢ ·fn = ( 𝑓 ∈ ℂ , 𝑔 ∈ ( ℂ ↑m ℋ ) ↦ ( 𝑥 ∈ ℋ ↦ ( 𝑓 · ( 𝑔 ‘ 𝑥 ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | chft | ⊢ ·fn | |
| 1 | vf | ⊢ 𝑓 | |
| 2 | cc | ⊢ ℂ | |
| 3 | vg | ⊢ 𝑔 | |
| 4 | cmap | ⊢ ↑m | |
| 5 | chba | ⊢ ℋ | |
| 6 | 2 5 4 | co | ⊢ ( ℂ ↑m ℋ ) |
| 7 | vx | ⊢ 𝑥 | |
| 8 | 1 | cv | ⊢ 𝑓 |
| 9 | cmul | ⊢ · | |
| 10 | 3 | cv | ⊢ 𝑔 |
| 11 | 7 | cv | ⊢ 𝑥 |
| 12 | 11 10 | cfv | ⊢ ( 𝑔 ‘ 𝑥 ) |
| 13 | 8 12 9 | co | ⊢ ( 𝑓 · ( 𝑔 ‘ 𝑥 ) ) |
| 14 | 7 5 13 | cmpt | ⊢ ( 𝑥 ∈ ℋ ↦ ( 𝑓 · ( 𝑔 ‘ 𝑥 ) ) ) |
| 15 | 1 3 2 6 14 | cmpo | ⊢ ( 𝑓 ∈ ℂ , 𝑔 ∈ ( ℂ ↑m ℋ ) ↦ ( 𝑥 ∈ ℋ ↦ ( 𝑓 · ( 𝑔 ‘ 𝑥 ) ) ) ) |
| 16 | 0 15 | wceq | ⊢ ·fn = ( 𝑓 ∈ ℂ , 𝑔 ∈ ( ℂ ↑m ℋ ) ↦ ( 𝑥 ∈ ℋ ↦ ( 𝑓 · ( 𝑔 ‘ 𝑥 ) ) ) ) |