homcl

Description: Closure of the scalar product of a Hilbert space operator. (Contributed by NM, 20-Feb-2006) (New usage is discouraged.)

		Ref	Expression
	Assertion	homcl	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ \land B \in ℋ) \to (A \cdot_{op} T) (B) \in ℋ$

Step	Hyp	Ref	Expression
1		homval	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ \land B \in ℋ) \to (A \cdot_{op} T) (B) = A \cdot_{ℎ} T (B)$
2		ffvelrn	$⊢ (T : ℋ ⟶ ℋ \land B \in ℋ) \to T (B) \in ℋ$
3	2	anim2i	$⊢ (A \in ℂ \land (T : ℋ ⟶ ℋ \land B \in ℋ)) \to (A \in ℂ \land T (B) \in ℋ)$
4	3	3impb	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ \land B \in ℋ) \to (A \in ℂ \land T (B) \in ℋ)$
5		hvmulcl	$⊢ (A \in ℂ \land T (B) \in ℋ) \to A \cdot_{ℎ} T (B) \in ℋ$
6	4 5	syl	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ \land B \in ℋ) \to A \cdot_{ℎ} T (B) \in ℋ$
7	1 6	eqeltrd	$⊢ (A \in ℂ \land T : ℋ ⟶ ℋ \land B \in ℋ) \to (A \cdot_{op} T) (B) \in ℋ$

Metamath Proof Explorer