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