Theorem hfmval

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

	Ref	Expression
Assertion	hfmval	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 : ℋ ⟶ ℂ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 ·fn 𝑇 ) ‘ 𝐵 ) = ( 𝐴 · ( 𝑇 ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		hfmmval	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 : ℋ ⟶ ℂ ) → ( 𝐴 ·fn 𝑇 ) = ( 𝑥 ∈ ℋ ↦ ( 𝐴 · ( 𝑇 ‘ 𝑥 ) ) ) )
2	1	fveq1d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 : ℋ ⟶ ℂ ) → ( ( 𝐴 ·fn 𝑇 ) ‘ 𝐵 ) = ( ( 𝑥 ∈ ℋ ↦ ( 𝐴 · ( 𝑇 ‘ 𝑥 ) ) ) ‘ 𝐵 ) )
3		fveq2	⊢ ( 𝑥 = 𝐵 → ( 𝑇 ‘ 𝑥 ) = ( 𝑇 ‘ 𝐵 ) )
4	3	oveq2d	⊢ ( 𝑥 = 𝐵 → ( 𝐴 · ( 𝑇 ‘ 𝑥 ) ) = ( 𝐴 · ( 𝑇 ‘ 𝐵 ) ) )
5		eqid	⊢ ( 𝑥 ∈ ℋ ↦ ( 𝐴 · ( 𝑇 ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℋ ↦ ( 𝐴 · ( 𝑇 ‘ 𝑥 ) ) )
6		ovex	⊢ ( 𝐴 · ( 𝑇 ‘ 𝐵 ) ) ∈ V
7	4 5 6	fvmpt	⊢ ( 𝐵 ∈ ℋ → ( ( 𝑥 ∈ ℋ ↦ ( 𝐴 · ( 𝑇 ‘ 𝑥 ) ) ) ‘ 𝐵 ) = ( 𝐴 · ( 𝑇 ‘ 𝐵 ) ) )
8	2 7	sylan9eq	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑇 : ℋ ⟶ ℂ ) ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 ·fn 𝑇 ) ‘ 𝐵 ) = ( 𝐴 · ( 𝑇 ‘ 𝐵 ) ) )
9	8	3impa	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 : ℋ ⟶ ℂ ∧ 𝐵 ∈ ℋ ) → ( ( 𝐴 ·fn 𝑇 ) ‘ 𝐵 ) = ( 𝐴 · ( 𝑇 ‘ 𝐵 ) ) )