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 = ( 𝑓 ∈ ℂ , 𝑔 ∈ ( ℋ ↑m ℋ ) ↦ ( 𝑥 ∈ ℋ ↦ ( 𝑓 ·ℎ ( 𝑔 ‘ 𝑥 ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | chot | ⊢ ·op | |
| 1 | vf | ⊢ 𝑓 | |
| 2 | cc | ⊢ ℂ | |
| 3 | vg | ⊢ 𝑔 | |
| 4 | chba | ⊢ ℋ | |
| 5 | cmap | ⊢ ↑m | |
| 6 | 4 4 5 | co | ⊢ ( ℋ ↑m ℋ ) |
| 7 | vx | ⊢ 𝑥 | |
| 8 | 1 | cv | ⊢ 𝑓 |
| 9 | csm | ⊢ ·ℎ | |
| 10 | 3 | cv | ⊢ 𝑔 |
| 11 | 7 | cv | ⊢ 𝑥 |
| 12 | 11 10 | cfv | ⊢ ( 𝑔 ‘ 𝑥 ) |
| 13 | 8 12 9 | co | ⊢ ( 𝑓 ·ℎ ( 𝑔 ‘ 𝑥 ) ) |
| 14 | 7 4 13 | cmpt | ⊢ ( 𝑥 ∈ ℋ ↦ ( 𝑓 ·ℎ ( 𝑔 ‘ 𝑥 ) ) ) |
| 15 | 1 3 2 6 14 | cmpo | ⊢ ( 𝑓 ∈ ℂ , 𝑔 ∈ ( ℋ ↑m ℋ ) ↦ ( 𝑥 ∈ ℋ ↦ ( 𝑓 ·ℎ ( 𝑔 ‘ 𝑥 ) ) ) ) |
| 16 | 0 15 | wceq | ⊢ ·op = ( 𝑓 ∈ ℂ , 𝑔 ∈ ( ℋ ↑m ℋ ) ↦ ( 𝑥 ∈ ℋ ↦ ( 𝑓 ·ℎ ( 𝑔 ‘ 𝑥 ) ) ) ) |