This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑇 ) = ( 𝑥 ∈ ℋ ↦ ( 𝐴 · ( 𝑇 ‘ 𝑥 ) ) ) )