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 ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ → A · op T = x ∈ ℋ ⟼ A ⋅ ℎ T ⁡ x

Proof

Step Hyp Ref Expression
1 ax-hilex ⊢ ℋ ∈ V
2 1 1 elmap ⊢ T ∈ ℋ ℋ ↔ T : ℋ ⟶ ℋ
3 oveq1 ⊢ f = A → f ⋅ ℎ g ⁡ x = A ⋅ ℎ g ⁡ x
4 3 mpteq2dv ⊢ f = A → x ∈ ℋ ⟼ f ⋅ ℎ g ⁡ x = x ∈ ℋ ⟼ A ⋅ ℎ g ⁡ x
5 fveq1 ⊢ g = T → g ⁡ x = T ⁡ x
6 5 oveq2d ⊢ g = T → A ⋅ ℎ g ⁡ x = A ⋅ ℎ T ⁡ x
7 6 mpteq2dv ⊢ g = T → x ∈ ℋ ⟼ A ⋅ ℎ g ⁡ x = x ∈ ℋ ⟼ A ⋅ ℎ T ⁡ x
8 df-homul ⊢ · op = f ∈ ℂ , g ∈ ℋ ℋ ⟼ x ∈ ℋ ⟼ f ⋅ ℎ g ⁡ x
9 1 mptex ⊢ x ∈ ℋ ⟼ A ⋅ ℎ T ⁡ x ∈ V
10 4 7 8 9 ovmpo ⊢ A ∈ ℂ ∧ T ∈ ℋ ℋ → A · op T = x ∈ ℋ ⟼ A ⋅ ℎ T ⁡ x
11 2 10 sylan2br ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ → A · op T = x ∈ ℋ ⟼ A ⋅ ℎ T ⁡ x