Axiom ax-hfvmul 8814

Description: Scalar multiplication is an operation on ℂ and ℋ.

Assertion

Ref	Expression
ax-hfvmul	⊢ ·h :(ℂ × ℋ )–→ ℋ

Detailed syntax breakdown of Axiom ax-hfvmul

Step	Hyp	Ref	Expression
1		cc 5212	. . 3 class ℂ
2		chil 8727	. . 3 class ℋ
3	1, 2	cxp 3163	. 2 class (ℂ × ℋ )
4		csm 8729	. 2 class ·h
5	3, 2, 4	wf 3173	1 wff ·h :(ℂ × ℋ )–→ ℋ

This axiom is referenced by:  hvmulex 8820  hvmulclt 8822  hilvc 8968  hhssabl 9071  hhssnv 9073  hhsssh 9078

Copyright terms: Public domain