Axiom ax-hfvmul 10507

Description: Scalar multiplication is an operation on CC and ~H.

Assertion

Ref	Expression
ax-hfvmul	|- .h :(CC X. ~H)-->~H

Detailed syntax breakdown of Axiom ax-hfvmul

Step	Hyp	Ref	Expression
1		cc 6384	. . 3 class CC
2		chil 10420	. . 3 class ~H
3	1, 2	cxp 3984	. 2 class (CC X. ~H)
4		csm 10422	. 2 class .h
5	3, 2, 4	wf 3994	1 wff .h :(CC X. ~H)-->~H

This axiom is referenced by:  hvmulex 10513  hvmulcl 10515  hilvc 10662  hhssabli 10765  hhssnv 10767  hhsssh 10772

Copyright terms: Public domain