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 ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\to {A}{·}_{\mathrm{op}}{T}=\left({x}\in ℋ⟼{A}{\cdot }_{ℎ}{T}\left({x}\right)\right)$

Proof

Step Hyp Ref Expression
1 ax-hilex ${⊢}ℋ\in \mathrm{V}$
2 1 1 elmap ${⊢}{T}\in \left({ℋ}^{ℋ}\right)↔{T}:ℋ⟶ℋ$
3 oveq1 ${⊢}{f}={A}\to {f}{\cdot }_{ℎ}{g}\left({x}\right)={A}{\cdot }_{ℎ}{g}\left({x}\right)$
4 3 mpteq2dv ${⊢}{f}={A}\to \left({x}\in ℋ⟼{f}{\cdot }_{ℎ}{g}\left({x}\right)\right)=\left({x}\in ℋ⟼{A}{\cdot }_{ℎ}{g}\left({x}\right)\right)$
5 fveq1 ${⊢}{g}={T}\to {g}\left({x}\right)={T}\left({x}\right)$
6 5 oveq2d ${⊢}{g}={T}\to {A}{\cdot }_{ℎ}{g}\left({x}\right)={A}{\cdot }_{ℎ}{T}\left({x}\right)$
7 6 mpteq2dv ${⊢}{g}={T}\to \left({x}\in ℋ⟼{A}{\cdot }_{ℎ}{g}\left({x}\right)\right)=\left({x}\in ℋ⟼{A}{\cdot }_{ℎ}{T}\left({x}\right)\right)$
8 df-homul ${⊢}{·}_{\mathrm{op}}=\left({f}\in ℂ,{g}\in \left({ℋ}^{ℋ}\right)⟼\left({x}\in ℋ⟼{f}{\cdot }_{ℎ}{g}\left({x}\right)\right)\right)$
9 1 mptex ${⊢}\left({x}\in ℋ⟼{A}{\cdot }_{ℎ}{T}\left({x}\right)\right)\in \mathrm{V}$
10 4 7 8 9 ovmpo ${⊢}\left({A}\in ℂ\wedge {T}\in \left({ℋ}^{ℋ}\right)\right)\to {A}{·}_{\mathrm{op}}{T}=\left({x}\in ℋ⟼{A}{\cdot }_{ℎ}{T}\left({x}\right)\right)$
11 2 10 sylan2br ${⊢}\left({A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\to {A}{·}_{\mathrm{op}}{T}=\left({x}\in ℋ⟼{A}{\cdot }_{ℎ}{T}\left({x}\right)\right)$