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

Metamath Proof Explorer

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 𝑇 ) ‘ 𝐵 ) = ( 𝐴 · ( 𝑇 ‘ 𝐵 ) ) )