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	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( 𝐴 ·op 𝑇 ) = ( 𝑥 ∈ ℋ ↦ ( 𝐴 ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		ax-hilex	⊢ ℋ ∈ V
2	1 1	elmap	⊢ ( 𝑇 ∈ ( ℋ ↑m ℋ ) ↔ 𝑇 : ℋ ⟶ ℋ )
3		oveq1	⊢ ( 𝑓 = 𝐴 → ( 𝑓 ·ℎ ( 𝑔 ‘ 𝑥 ) ) = ( 𝐴 ·ℎ ( 𝑔 ‘ 𝑥 ) ) )
4	3	mpteq2dv	⊢ ( 𝑓 = 𝐴 → ( 𝑥 ∈ ℋ ↦ ( 𝑓 ·ℎ ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℋ ↦ ( 𝐴 ·ℎ ( 𝑔 ‘ 𝑥 ) ) ) )
5		fveq1	⊢ ( 𝑔 = 𝑇 → ( 𝑔 ‘ 𝑥 ) = ( 𝑇 ‘ 𝑥 ) )
6	5	oveq2d	⊢ ( 𝑔 = 𝑇 → ( 𝐴 ·ℎ ( 𝑔 ‘ 𝑥 ) ) = ( 𝐴 ·ℎ ( 𝑇 ‘ 𝑥 ) ) )
7	6	mpteq2dv	⊢ ( 𝑔 = 𝑇 → ( 𝑥 ∈ ℋ ↦ ( 𝐴 ·ℎ ( 𝑔 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℋ ↦ ( 𝐴 ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) )
8		df-homul	⊢ ·op = ( 𝑓 ∈ ℂ , 𝑔 ∈ ( ℋ ↑m ℋ ) ↦ ( 𝑥 ∈ ℋ ↦ ( 𝑓 ·ℎ ( 𝑔 ‘ 𝑥 ) ) ) )
9	1	mptex	⊢ ( 𝑥 ∈ ℋ ↦ ( 𝐴 ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) ∈ V
10	4 7 8 9	ovmpo	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 ∈ ( ℋ ↑m ℋ ) ) → ( 𝐴 ·op 𝑇 ) = ( 𝑥 ∈ ℋ ↦ ( 𝐴 ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) )
11	2 10	sylan2br	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( 𝐴 ·op 𝑇 ) = ( 𝑥 ∈ ℋ ↦ ( 𝐴 ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) )