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

Metamath Proof Explorer

Theorem homulcl

Description: The scalar product of a Hilbert space operator is an operator. (Contributed by NM, 21-Feb-2006) (Revised by Mario Carneiro, 16-Nov-2013) (New usage is discouraged.)

Ref Expression
Assertion homulcl ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ → A · op T : ℋ ⟶ ℋ

Proof

Step Hyp Ref Expression
1 ffvelcdm ⊢ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → T ⁡ x ∈ ℋ
2 hvmulcl ⊢ A ∈ ℂ ∧ T ⁡ x ∈ ℋ → A ⋅ ℎ T ⁡ x ∈ ℋ
3 1 2 sylan2 ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → A ⋅ ℎ T ⁡ x ∈ ℋ
4 3 anassrs ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → A ⋅ ℎ T ⁡ x ∈ ℋ
5 4 fmpttd ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ → x ∈ ℋ ⟼ A ⋅ ℎ T ⁡ x : ℋ ⟶ ℋ
6 hommval ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ → A · op T = x ∈ ℋ ⟼ A ⋅ ℎ T ⁡ x
7 6 feq1d ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ → A · op T : ℋ ⟶ ℋ ↔ x ∈ ℋ ⟼ A ⋅ ℎ T ⁡ x : ℋ ⟶ ℋ
8 5 7 mpbird ⊢ A ∈ ℂ ∧ T : ℋ ⟶ ℋ → A · op T : ℋ ⟶ ℋ