Axiom ax-hfvmul 30121

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

Assertion

Ref	Expression
ax-hfvmul	⊢ ·ℎ :(ℂ × ℋ)⟶ ℋ

Detailed syntax breakdown of Axiom ax-hfvmul

Step	Hyp	Ref	Expression
1		cc 11090	. . 3 class ℂ
2		chba 30035	. . 3 class ℋ
3	1, 2	cxp 5667	. 2 class (ℂ × ℋ)
4		csm 30037	. 2 class ·ℎ
5	3, 2, 4	wf 6528	1 wff ·ℎ :(ℂ × ℋ)⟶ ℋ

This axiom is referenced by:  hvmulex  30127  hvmulcl  30129  hilvc  30278  issh2  30325  hhssabloilem  30377  hhssnv  30380  hhsssh  30385