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

Metamath Proof Explorer

Theorem hvmulcl

Description: Closure of scalar multiplication. (Contributed by NM, 19-Apr-2007) (New usage is discouraged.)

		Ref	Expression
	Assertion	hvmulcl	$⊢ (A \in ℂ \land B \in ℋ) \to A \cdot_{ℎ} B \in ℋ$

Step	Hyp	Ref	Expression
1		ax-hfvmul	$⊢ \cdot_{ℎ} : ℂ \times ℋ ⟶ ℋ$
2	1	fovcl	$⊢ (A \in ℂ \land B \in ℋ) \to A \cdot_{ℎ} B \in ℋ$