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	$$⊢{·}_{\mathrm{op}}=\left(f\in ℂ,g\in \left({\mathscr{H}}^{\mathscr{H}}\right)⟼\left(x\in \mathscr{H}⟼f{\cdot }_{ℎ}g\left(x\right)\right)\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		chot	$$class{·}_{\mathrm{op}}$$
1		vf	$$setvarf$$
2		cc	$$classℂ$$
3		vg	$$setvarg$$
4		chba	$$class\mathscr{H}$$
5		cmap	$$class{\uparrow }_{𝑚}$$
6	4 4 5	co	$$class\left({\mathscr{H}}^{\mathscr{H}}\right)$$
7		vx	$$setvarx$$
8	1	cv	$$setvarf$$
9		csm	$$class{\cdot }_{ℎ}$$
10	3	cv	$$setvarg$$
11	7	cv	$$setvarx$$
12	11 10	cfv	$$classg\left(x\right)$$
13	8 12 9	co	$$class\left(f{\cdot }_{ℎ}g\left(x\right)\right)$$
14	7 4 13	cmpt	$$class\left(x\in \mathscr{H}⟼f{\cdot }_{ℎ}g\left(x\right)\right)$$
15	1 3 2 6 14	cmpo	$$class\left(f\in ℂ,g\in \left({\mathscr{H}}^{\mathscr{H}}\right)⟼\left(x\in \mathscr{H}⟼f{\cdot }_{ℎ}g\left(x\right)\right)\right)$$
16	0 15	wceq	$$wff{·}_{\mathrm{op}}=\left(f\in ℂ,g\in \left({\mathscr{H}}^{\mathscr{H}}\right)⟼\left(x\in \mathscr{H}⟼f{\cdot }_{ℎ}g\left(x\right)\right)\right)$$