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

Metamath Proof Explorer

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