Theorem homval

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

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

Proof

Step	Hyp	Ref	Expression
1		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)$$
2	1	fveq1d	$$⊢\left(A\in ℂ\wedge T:\mathscr{H}⟶\mathscr{H}\right)\to \left(A{·}_{\mathrm{op}}T\right)\left(B\right)=\left(x\in \mathscr{H}⟼A{\cdot }_{ℎ}T\left(x\right)\right)\left(B\right)$$
3		fveq2	$$⊢x=B\to T\left(x\right)=T\left(B\right)$$
4	3	oveq2d	$$⊢x=B\to A{\cdot }_{ℎ}T\left(x\right)=A{\cdot }_{ℎ}T\left(B\right)$$
5		eqid	$$⊢\left(x\in \mathscr{H}⟼A{\cdot }_{ℎ}T\left(x\right)\right)=\left(x\in \mathscr{H}⟼A{\cdot }_{ℎ}T\left(x\right)\right)$$
6		ovex	$$⊢A{\cdot }_{ℎ}T\left(B\right)\in \mathrm{V}$$
7	4 5 6	fvmpt	$$⊢B\in \mathscr{H}\to \left(x\in \mathscr{H}⟼A{\cdot }_{ℎ}T\left(x\right)\right)\left(B\right)=A{\cdot }_{ℎ}T\left(B\right)$$
8	2 7	sylan9eq	$$⊢\left(\left(A\in ℂ\wedge T:\mathscr{H}⟶\mathscr{H}\right)\wedge B\in \mathscr{H}\right)\to \left(A{·}_{\mathrm{op}}T\right)\left(B\right)=A{\cdot }_{ℎ}T\left(B\right)$$
9	8	3impa	$$⊢\left(A\in ℂ\wedge T:\mathscr{H}⟶\mathscr{H}\wedge B\in \mathscr{H}\right)\to \left(A{·}_{\mathrm{op}}T\right)\left(B\right)=A{\cdot }_{ℎ}T\left(B\right)$$