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	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( 𝐴 ·op 𝑇 ) : ℋ ⟶ ℋ )

Proof

Step	Hyp	Ref	Expression
1		ffvelrn	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
2		hvmulcl	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑇 ‘ 𝑥 ) ∈ ℋ ) → ( 𝐴 ·ℎ ( 𝑇 ‘ 𝑥 ) ) ∈ ℋ )
3	1 2	sylan2	⊢ ( ( 𝐴 ∈ ℂ ∧ ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) ) → ( 𝐴 ·ℎ ( 𝑇 ‘ 𝑥 ) ) ∈ ℋ )
4	3	anassrs	⊢ ( ( ( 𝐴 ∈ ℂ ∧ 𝑇 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( 𝐴 ·ℎ ( 𝑇 ‘ 𝑥 ) ) ∈ ℋ )
5	4	fmpttd	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( 𝑥 ∈ ℋ ↦ ( 𝐴 ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) : ℋ ⟶ ℋ )
6		hommval	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( 𝐴 ·op 𝑇 ) = ( 𝑥 ∈ ℋ ↦ ( 𝐴 ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) )
7	6	feq1d	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( ( 𝐴 ·op 𝑇 ) : ℋ ⟶ ℋ ↔ ( 𝑥 ∈ ℋ ↦ ( 𝐴 ·ℎ ( 𝑇 ‘ 𝑥 ) ) ) : ℋ ⟶ ℋ ) )
8	5 7	mpbird	⊢ ( ( 𝐴 ∈ ℂ ∧ 𝑇 : ℋ ⟶ ℋ ) → ( 𝐴 ·op 𝑇 ) : ℋ ⟶ ℋ )