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

Metamath Proof Explorer

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