This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ℋ ⟶ ℋ$

Step	Hyp	Ref	Expression
0		csm	$class \cdot_{ℎ}$
1		cc	$class ℂ$
2		chba	$class ℋ$
3	1 2	cxp	$class (ℂ \times ℋ)$
4	3 2 0	wf	$wff \cdot_{ℎ} : ℂ \times ℋ ⟶ ℋ$