Theorem hfmmval

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

	Ref	Expression
Assertion	hfmmval	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 : ℋ ⟶ ℂ ) → ( 𝐴 ·fn 𝑇 ) = ( 𝑥 ∈ ℋ ↦ ( 𝐴 · ( 𝑇 ‘ 𝑥 ) ) ) )

Proof

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