Axiom ax-hfvmul

Description: Scalar multiplication is an operation on CC and ~H . (Contributed by NM, 16-Aug-1999) (New usage is discouraged.)

	Ref	Expression
Assertion	ax-hfvmul	$$⊢{\cdot }_{ℎ}:ℂ\times \mathscr{H}⟶\mathscr{H}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csm	$$class{\cdot }_{ℎ}$$
1		cc	$$classℂ$$
2		chba	$$class\mathscr{H}$$
3	1 2	cxp	$$class\left(ℂ\times \mathscr{H}\right)$$
4	3 2 0	wf	$$wff{\cdot }_{ℎ}:ℂ\times \mathscr{H}⟶\mathscr{H}$$