Theorem hvmulex

Description: The Hilbert space scalar product operation is a set. (Contributed by NM, 17-Apr-2007) (New usage is discouraged.)

	Ref	Expression
Assertion	hvmulex	⊢ ·ℎ ∈ V

Proof

Step	Hyp	Ref	Expression
1		ax-hfvmul	⊢ ·ℎ : ( ℂ × ℋ ) ⟶ ℋ
2		cnex	⊢ ℂ ∈ V
3		ax-hilex	⊢ ℋ ∈ V
4	2 3	xpex	⊢ ( ℂ × ℋ ) ∈ V
5		fex	⊢ ( ( ·ℎ : ( ℂ × ℋ ) ⟶ ℋ ∧ ( ℂ × ℋ ) ∈ V ) → ·ℎ ∈ V )
6	1 4 5	mp2an	⊢ ·ℎ ∈ V