Theorem hommval

Description: Value of the scalar product with a Hilbert space operator. (Contributed by NM, 20-Feb-2006) (Revised by Mario Carneiro, 23-Aug-2014) (New usage is discouraged.)

	Ref	Expression
Assertion	hommval	$$⊢\left(A\in ℂ\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to A{·}_{\mathrm{op}}T=\left(x\in \mathscr{H}⟼A{\cdot }_{ℎ}T\left(x\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		ax-hilex	$$⊢\mathscr{H}\in \mathrm{V}$$
2	1 1	elmap	$$⊢T\in \left({\mathscr{H}}^{\mathscr{H}}\right)\leftrightarrow T:\mathscr{H}⟶\mathscr{H}$$
3		oveq1	$$⊢f=A\to f{\cdot }_{ℎ}g\left(x\right)=A{\cdot }_{ℎ}g\left(x\right)$$
4	3	mpteq2dv	$$⊢f=A\to \left(x\in \mathscr{H}⟼f{\cdot }_{ℎ}g\left(x\right)\right)=\left(x\in \mathscr{H}⟼A{\cdot }_{ℎ}g\left(x\right)\right)$$
5		fveq1	$$⊢g=T\to g\left(x\right)=T\left(x\right)$$
6	5	oveq2d	$$⊢g=T\to A{\cdot }_{ℎ}g\left(x\right)=A{\cdot }_{ℎ}T\left(x\right)$$
7	6	mpteq2dv	$$⊢g=T\to \left(x\in \mathscr{H}⟼A{\cdot }_{ℎ}g\left(x\right)\right)=\left(x\in \mathscr{H}⟼A{\cdot }_{ℎ}T\left(x\right)\right)$$
8		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)$$
9	1	mptex	$$⊢\left(x\in \mathscr{H}⟼A{\cdot }_{ℎ}T\left(x\right)\right)\in \mathrm{V}$$
10	4 7 8 9	ovmpo	$$⊢\left(A\in ℂ\wedge T\in \left({\mathscr{H}}^{\mathscr{H}}\right)\right)\to A{·}_{\mathrm{op}}T=\left(x\in \mathscr{H}⟼A{\cdot }_{ℎ}T\left(x\right)\right)$$
11	2 10	sylan2br	$$⊢\left(A\in ℂ\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to A{·}_{\mathrm{op}}T=\left(x\in \mathscr{H}⟼A{\cdot }_{ℎ}T\left(x\right)\right)$$