Definition df-homul

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 ℋ ) ↦ ( 𝑥 ∈ ℋ ↦ ( 𝑓 ·ℎ ( 𝑔 ‘ 𝑥 ) ) ) )

Detailed syntax breakdown

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 ℋ ) ↦ ( 𝑥 ∈ ℋ ↦ ( 𝑓 ·ℎ ( 𝑔 ‘ 𝑥 ) ) ) )