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	$$⊢{\cdot }_{ℎ}\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		ax-hfvmul	$$⊢{\cdot }_{ℎ}:ℂ\times \mathscr{H}⟶\mathscr{H}$$
2		cnex	$$⊢ℂ\in \mathrm{V}$$
3		ax-hilex	$$⊢\mathscr{H}\in \mathrm{V}$$
4	2 3	xpex	$$⊢ℂ\times \mathscr{H}\in \mathrm{V}$$
5		fex	$$⊢\left({\cdot }_{ℎ}:ℂ\times \mathscr{H}⟶\mathscr{H}\wedge ℂ\times \mathscr{H}\in \mathrm{V}\right)\to {\cdot }_{ℎ}\in \mathrm{V}$$
6	1 4 5	mp2an	$$⊢{\cdot }_{ℎ}\in \mathrm{V}$$