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

Metamath Proof Explorer

Theorem hicl

Description: Closure of inner product. (Contributed by NM, 17-Nov-2007) (New usage is discouraged.)

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

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