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	⊢ ·ℎ : ( ℂ × ℋ ) ⟶ ℋ

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csm	⊢ ·ℎ
1		cc	⊢ ℂ
2		chba	⊢ ℋ
3	1 2	cxp	⊢ ( ℂ × ℋ )
4	3 2 0	wf	⊢ ·ℎ : ( ℂ × ℋ ) ⟶ ℋ