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 
|- .h e. _V

Proof

Step Hyp Ref Expression
1 ax-hfvmul 
 |-  .h : ( CC X. ~H ) --> ~H
2 cnex 
 |-  CC e. _V
3 ax-hilex 
 |-  ~H e. _V
4 2 3 xpex 
 |-  ( CC X. ~H ) e. _V
5 fex 
 |-  ( ( .h : ( CC X. ~H ) --> ~H /\ ( CC X. ~H ) e. _V ) -> .h e. _V )
6 1 4 5 mp2an 
 |-  .h e. _V